Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
W
WSymb
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
GitLab community forum
Contribute to GitLab
Provide feedback
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
OTAWA-plugins
WSymb
Commits
0c97c20f
Commit
0c97c20f
authored
5 years ago
by
Forget Julien
Browse files
Options
Downloads
Patches
Plain Diff
Don't print a case: in loop_bounds(...) for symbolic loop bounds.
parent
ee50ac3c
Branches
Branches containing commit
No related tags found
No related merge requests found
Changes
3
Show whitespace changes
Inline
Side-by-side
Showing
3 changed files
simplify/symbol.ml
+12
-0
12 additions, 0 deletions
simplify/symbol.ml
simplify/to_c.ml
+5
-7
5 additions, 7 deletions
simplify/to_c.ml
simplify/wcet_formula.ml
+0
-12
0 additions, 12 deletions
simplify/wcet_formula.ml
with
17 additions
and
19 deletions
simplify/symbol.ml
+
12
−
0
View file @
0c97c20f
...
...
@@ -23,6 +23,18 @@ type param = string
(** Symbolic integer is either a constant or a symbol *)
type
symb_int
=
SInt
of
int
|
SParam
of
param
(* Returns true if sint is a symbol. *)
let
is_symb
sint
=
match
sint
with
|
SInt
_
->
false
|
SParam
_
->
true
(* Returns the constant corresponding to [sint]. Fails if [sint] is a symbol. *)
let
int_of_symb
sint
=
match
sint
with
|
SInt
i
->
i
|
SParam
_
->
Utils
.
internal_error
"int_of_symb"
"cannot be applied to param"
open
Format
let
pp_param
out_f
p
=
...
...
This diff is collapsed.
Click to expand it.
simplify/to_c.ml
+
5
−
7
View file @
0c97c20f
...
...
@@ -18,13 +18,11 @@ let c_array pp_elem ty_string out_f array =
pp_elem
out_f
)
array
let
c_symb_int
out_f
sint
=
match
sint
with
|
SInt
i
->
pp_print_int
out_f
i
|
SParam
p
->
pp_print_text
out_f
p
let
c_loop_bound
out_f
lname
bound
=
fprintf
out_f
"case %s: return %a;@ "
lname
c_symb_int
bound
match
bound
with
|
SInt
i
->
fprintf
out_f
"case %s: return %d;@ "
lname
i
|
SParam
_
->
()
let
c_loop_bounds
out_f
bounds
=
fprintf
out_f
"@[<v 2>int loop_bounds(int loop_id) {@ "
;
...
...
This diff is collapsed.
Click to expand it.
simplify/wcet_formula.ml
+
0
−
12
View file @
0c97c20f
...
...
@@ -36,18 +36,6 @@ type t =
let
bot_f
=
FConst
bot_wcet
(* Returns true if sint is a symbol. *)
let
is_symb
sint
=
match
sint
with
|
SInt
_
->
false
|
SParam
_
->
true
(* Returns the constant corresponding to [sint]. Fails if [sint] is a symbol. *)
let
int_of_symb
sint
=
match
sint
with
|
SInt
i
->
i
|
SParam
_
->
Utils
.
internal_error
"int_of_symb"
"cannot be applied to param"
(* Pretty printing *)
open
Format
...
...
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