Skip to content
GitLab
Explore
Sign in
Register
Primary navigation
Search or go to…
Project
C
cortex-m-rtfm-klee
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Wiki
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Snippets
Build
Pipelines
Jobs
Pipeline schedules
Artifacts
Deploy
Releases
Model registry
Operate
Environments
Monitor
Incidents
Analyze
Value stream analytics
Contributor analytics
CI/CD analytics
Repository analytics
Model experiments
Help
Help
Support
GitLab documentation
Compare GitLab plans
Community forum
Contribute to GitLab
Provide feedback
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
KLEE
cortex-m-rtfm-klee
Commits
a21de008
Commit
a21de008
authored
7 years ago
by
Per Lindgren
Browse files
Options
Downloads
Patches
Plain Diff
exam v1
parent
0991e740
No related branches found
No related tags found
No related merge requests found
Changes
1
Show whitespace changes
Inline
Side-by-side
Showing
1 changed file
gdb.py
+20
-1
20 additions, 1 deletion
gdb.py
with
20 additions
and
1 deletion
gdb.py
+
20
−
1
View file @
a21de008
...
@@ -678,7 +678,7 @@ gdb.execute("continue")
...
@@ -678,7 +678,7 @@ gdb.execute("continue")
# Your implementation should be generic though
# Your implementation should be generic though
# Looking up the WCETs from the `output_data`.
# Looking up the WCETs from the `output_data`.
# (It may be a good idea to make first pass and extract wcet per task)
# (It may be a good idea to make first pass and extract wcet per task)
#
#
#
# The total utilisation bound allows us to discard task sets that are
# The total utilisation bound allows us to discard task sets that are
# obviously illegal (not the case here though)
# obviously illegal (not the case here though)
#
#
...
@@ -752,6 +752,7 @@ gdb.execute("continue")
...
@@ -752,6 +752,7 @@ gdb.execute("continue")
# Verify that that the results are correct by hand computation (or make an Excel)
# Verify that that the results are correct by hand computation (or make an Excel)
#
#
# Assignment 4.
# Assignment 4.
#
# Looking closer at 7.22 we see that its a recurrent equation.
# Looking closer at 7.22 we see that its a recurrent equation.
# Ri(0) indicating the initial value
# Ri(0) indicating the initial value
# Ri(0) = Ci + Bi
# Ri(0) = Ci + Bi
...
@@ -795,3 +796,21 @@ gdb.execute("continue")
...
@@ -795,3 +796,21 @@ gdb.execute("continue")
# Assignment 2, 10 points
# Assignment 2, 10 points
# Assignment 3, 10 points
# Assignment 3, 10 points
# Assignment 4, 15 points
# Assignment 4, 15 points
#
# To make sure the analysis works in the general case
# you can make further examles based on 'resource.rs'
#
# Notice, KLEE analysis does not work on hardware peripherals
# (this is not yet supported), so your new examples must NOT access
# any peripherals.
#
# HINTS
# You may start by cut and paste the output (table) to a file 'x.py'
#
# Implement the analysis in a seprate python file 'x.py'
# (reconstruct the 'outputdata' from the table)
#
# When you have your analysis working,
# integrate it in this script (operating on the real 'outputdata')
#
#
This diff is collapsed.
Click to expand it.
Preview
0%
Loading
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Save comment
Cancel
Please
register
or
sign in
to comment