Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
F
frama-c
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Wiki
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Snippets
Deploy
Releases
Package Registry
Container Registry
Model registry
Operate
Terraform modules
Monitor
Incidents
Analyze
Value stream analytics
Contributor 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
Charles Southerland
frama-c
Commits
57e7bde1
Commit
57e7bde1
authored
4 years ago
by
Valentin Perrelle
Committed by
Virgile Prevosto
4 years ago
Browse files
Options
Downloads
Patches
Plain Diff
[Aorai] do not rely on Aorai internal tables for Frama_C_show_aorai_state
parent
b99bc098
No related branches found
No related tags found
No related merge requests found
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
src/plugins/aorai/aorai_eva_analysis.enabled.ml
+22
-3
22 additions, 3 deletions
src/plugins/aorai/aorai_eva_analysis.enabled.ml
with
22 additions
and
3 deletions
src/plugins/aorai/aorai_eva_analysis.enabled.ml
+
22
−
3
View file @
57e7bde1
...
@@ -23,13 +23,32 @@
...
@@ -23,13 +23,32 @@
(* *)
(* *)
(**************************************************************************)
(**************************************************************************)
let
state_name
ty
i
=
(* Data_for_aorai.getStateName (Integer.to_int i) *)
let
open
Cil_types
in
let
matching_enumitem
ei
=
match
Cil
.
isInteger
ei
.
eival
with
|
Some
j
->
Integer
.
equal
i
j
|
None
->
false
in
let
find_enumitem
e
=
List
.
find_opt
matching_enumitem
e
.
eitems
in
let
e
=
match
ty
with
|
TEnum
(
e
,_
)
->
Some
e
|
_
->
None
in
match
Extlib
.
opt_bind
find_enumitem
e
with
|
Some
ei
->
ei
.
eiorig_name
|
None
->
Integer
.
to_string
i
let
show_aorai_variable
state
fmt
var_name
=
let
show_aorai_variable
state
fmt
var_name
=
let
vi
=
Data_for_aorai
.(
get_varinfo
var_name
)
in
let
vi
=
Globals
.
Vars
.
find_from_astinfo
var_name
Cil_types
.
VGlobal
in
let
ty
=
Globals
.
Types
.
find_type
Logic_typing
.
Enum
Data_for_aorai
.
states
in
let
cvalue
=
!
Db
.
Value
.
eval_expr
state
(
Cil
.
evar
vi
)
in
let
cvalue
=
!
Db
.
Value
.
eval_expr
state
(
Cil
.
evar
vi
)
in
try
try
let
i
=
Ival
.
project_int
(
Cvalue
.
V
.
project_ival
cvalue
)
in
let
i
=
Ival
.
project_int
(
Cvalue
.
V
.
project_ival
cvalue
)
in
let
state_name
=
Data_for_aorai
.
getStateName
(
Integer
.
to_int
i
)
in
Format
.
fprintf
fmt
"%s"
(
state_name
ty
i
)
Format
.
fprintf
fmt
"%s"
state_name
with
Cvalue
.
V
.
Not_based_on_null
|
Ival
.
Not_Singleton_Int
|
with
Cvalue
.
V
.
Not_based_on_null
|
Ival
.
Not_Singleton_Int
|
Z
.
Overflow
|
Not_found
->
Z
.
Overflow
|
Not_found
->
Format
.
fprintf
fmt
"?"
Format
.
fprintf
fmt
"?"
...
...
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