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
Deploy
Releases
Container Registry
Model registry
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
pub
frama-c
Commits
a6dc8b9b
Commit
a6dc8b9b
authored
3 years ago
by
Virgile Prevosto
Browse files
Options
Downloads
Patches
Plain Diff
[aorai] get rid of unused definitions
parent
b142a947
No related branches found
No related tags found
No related merge requests found
Changes
3
Hide whitespace changes
Inline
Side-by-side
Showing
3 changed files
src/plugins/aorai/aorai_visitors.ml
+0
-8
0 additions, 8 deletions
src/plugins/aorai/aorai_visitors.ml
src/plugins/aorai/path_analysis.ml
+0
-37
0 additions, 37 deletions
src/plugins/aorai/path_analysis.ml
src/plugins/aorai/utils_parser.ml
+0
-58
0 additions, 58 deletions
src/plugins/aorai/utils_parser.ml
with
0 additions
and
103 deletions
src/plugins/aorai/aorai_visitors.ml
+
0
−
8
View file @
a6dc8b9b
...
@@ -41,14 +41,6 @@ let get_acceptance_pred () =
...
@@ -41,14 +41,6 @@ let get_acceptance_pred () =
|
Bool3
.
False
|
Bool3
.
Undefined
->
acc
)
|
Bool3
.
False
|
Bool3
.
Undefined
->
acc
)
Logic_const
.
pfalse
st
Logic_const
.
pfalse
st
let
get_call_name
exp
=
match
exp
.
enode
with
|
Const
(
CStr
(
s
))
->
s
|
Lval
(
Var
(
vi
)
,
NoOffset
)
->
vi
.
vname
|
_
->
Aorai_option
.
not_yet_implemented
~
source
:
(
fst
exp
.
eloc
)
"At this time, only explicit calls are allowed by the Aorai plugin."
(****************************************************************************)
(****************************************************************************)
(* The instrumentation is done in two passes:
(* The instrumentation is done in two passes:
...
...
This diff is collapsed.
Click to expand it.
src/plugins/aorai/path_analysis.ml
+
0
−
37
View file @
a6dc8b9b
...
@@ -73,27 +73,6 @@ let dijkstra (adj: 'a -> ('a * int) list) (v1:'a) (v2:'a) =
...
@@ -73,27 +73,6 @@ let dijkstra (adj: 'a -> ('a * int) list) (v1:'a) (v2:'a) =
in
in
loop
(
add
(
0
,
(
v1
,
[]
))
(
empty
()
))
loop
(
add
(
0
,
(
v1
,
[]
))
(
empty
()
))
let
existing_path
(
stl
,_
as
auto
)
stn1
stn2
=
let
st1
=
ref
(
List
.
hd
stl
)
in
let
st2
=
ref
(
List
.
hd
stl
)
in
List
.
iter
(
fun
st
->
if
st
.
nums
=
stn1
then
st1
:=
st
;
if
st
.
nums
=
stn2
then
st2
:=
st
;
)
stl
;
try
let
_
=
dijkstra
(
voisins
auto
)
!
st1
!
st2
in
true
with
|
Not_found
->
false
;;
(** since Nitrogen-20111001 *)
(** since Nitrogen-20111001 *)
let
get_transitions_of_state
st
(
_
,
tr
)
=
let
get_transitions_of_state
st
(
_
,
tr
)
=
List
.
fold_left
List
.
fold_left
...
@@ -101,12 +80,6 @@ let get_transitions_of_state st (_,tr) =
...
@@ -101,12 +80,6 @@ let get_transitions_of_state st (_,tr) =
if
tr
.
start
.
nums
=
st
.
nums
then
tr
::
acc
else
acc
)
if
tr
.
start
.
nums
=
st
.
nums
then
tr
::
acc
else
acc
)
[]
tr
[]
tr
let
get_transitions_to_state
st
(
_
,
tr
)
=
List
.
fold_left
(
fun
acc
tr
->
if
tr
.
stop
.
nums
=
st
.
nums
then
tr
::
acc
else
acc
)
[]
tr
let
get_edges
st1
st2
(
_
,
tr
)
=
let
get_edges
st1
st2
(
_
,
tr
)
=
List
.
find_all
List
.
find_all
(
fun
tr
->
tr
.
start
.
nums
=
st1
.
nums
&&
tr
.
stop
.
nums
=
st2
.
nums
)
(
fun
tr
->
tr
.
start
.
nums
=
st1
.
nums
&&
tr
.
stop
.
nums
=
st2
.
nums
)
...
@@ -131,16 +104,6 @@ let at_most_one_path (states,transitions as auto) st1 st2 =
...
@@ -131,16 +104,6 @@ let at_most_one_path (states,transitions as auto) st1 st2 =
false
false
with
Not_found
->
true
with
Not_found
->
true
let
test
(
stl
,_
as
auto
)
=
let
st2
=
List
.
hd
stl
in
let
st1
=
List
.
hd
(
List
.
tl
stl
)
in
Aorai_option
.
feedback
"test : Etats choisis (%d,%d)"
st1
.
nums
st2
.
nums
;
let
(
res
,_
)
=
dijkstra
(
voisins
auto
)
st1
st2
in
Aorai_option
.
feedback
"Fini.@
\n
%a"
(
Pretty_utils
.
pp_list
~
pre
:
"@[["
~
sep
:
",@ "
~
suf
:
"@]]"
(
fun
fmt
st
->
Format
.
fprintf
fmt
"%d"
st
.
nums
))
res
(*
(*
Local Variables:
Local Variables:
compile-command: "make -C ../../.."
compile-command: "make -C ../../.."
...
...
This diff is collapsed.
Click to expand it.
src/plugins/aorai/utils_parser.ml
+
0
−
58
View file @
a6dc8b9b
...
@@ -43,61 +43,3 @@ let newline lexbuf =
...
@@ -43,61 +43,3 @@ let newline lexbuf =
let
pos
=
lexbuf
.
lex_curr_p
in
let
pos
=
lexbuf
.
lex_curr_p
in
lexbuf
.
lex_curr_p
<-
lexbuf
.
lex_curr_p
<-
{
pos
with
pos_lnum
=
pos
.
pos_lnum
+
1
;
pos_bol
=
pos
.
pos_cnum
}
{
pos
with
pos_lnum
=
pos
.
pos_lnum
+
1
;
pos_bol
=
pos
.
pos_cnum
}
let
rec
get_last_field
my_field
my_offset
=
match
my_offset
with
|
Cil_types
.
NoOffset
->
my_field
|
Cil_types
.
Field
(
fieldinfo
,
the_offset
)
->
get_last_field
fieldinfo
the_offset
|
_
->
Aorai_option
.
fatal
"NOT YET IMPLEMENTED : struct with array access."
let
rec
add_offset
father_offset
new_offset
=
match
father_offset
with
|
Cil_types
.
NoOffset
->
new_offset
|
Cil_types
.
Field
(
_
,
the_offset
)
->
(
Cil
.
addOffset
father_offset
(
add_offset
the_offset
new_offset
))
|
_
->
Aorai_option
.
fatal
"NOT YET IMPLEMENTED : struct with array access."
let
rec
get_field_info_from_name
my_list
name
=
if
(
List
.
length
my_list
<>
0
)
then
begin
let
my_field
=
List
.
hd
my_list
in
if
(
my_field
.
Cil_types
.
fname
=
name
)
then
my_field
else
get_field_info_from_name
(
List
.
tl
my_list
)
name
end
else
Aorai_option
.
fatal
"no field found with name :%s"
name
let
get_new_offset
my_host
my_offset
name
=
match
my_host
with
|
Cil_types
.
Var
(
var
)
->
let
var_info
=
var
in
(* if my_offset is null no need to search the last field *)
(* else we need to have the last *)
let
my_comp
=
if
(
my_offset
=
Cil_types
.
NoOffset
)
then
match
var_info
.
Cil_types
.
vtype
with
|
Cil_types
.
TComp
(
mc
,_,_
)
->
mc
|
_
->
assert
false
(*Cil_types.TComp(my_comp,_,_) = var_info.Cil_types.vtype in*)
else
begin
let
get_field_from_offset
my_offset
=
begin
match
my_offset
with
|
Cil_types
.
Field
(
fieldinfo
,_
)
->
fieldinfo
|
_
->
Aorai_option
.
fatal
"support only struct no array with struct"
end
in
let
field_info
=
get_field_from_offset
my_offset
in
let
last_field_offset
=
get_last_field
field_info
my_offset
in
(* last field in offset but not the field we want, for that we search in*)
let
mc
=
last_field_offset
.
Cil_types
.
fcomp
in
mc
end
in
let
cfields
=
Option
.
value
~
default
:
[]
my_comp
.
Cil_types
.
cfields
in
let
field_info
=
get_field_info_from_name
cfields
name
in
Cil_types
.
Field
(
field_info
,
Cil_types
.
NoOffset
)
|
_
->
Aorai_option
.
fatal
"NOT YET IMPLEMENTED : mem is not supported"
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