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
31ca77be
Commit
31ca77be
authored
2 years ago
by
Valentin Perrelle
Browse files
Options
Downloads
Patches
Plain Diff
[Cil_builder] Slight improvement of error handling for Stateful
parent
8aa8ef51
No related branches found
Branches containing commit
No related tags found
Tags containing commit
No related merge requests found
Changes
2
Hide whitespace changes
Inline
Side-by-side
Showing
2 changed files
src/kernel_services/ast_building/cil_builder.ml
+21
-18
21 additions, 18 deletions
src/kernel_services/ast_building/cil_builder.ml
src/kernel_services/ast_building/cil_builder.mli
+1
-1
1 addition, 1 deletion
src/kernel_services/ast_building/cil_builder.mli
with
22 additions
and
19 deletions
src/kernel_services/ast_building/cil_builder.ml
+
21
−
18
View file @
31ca77be
...
@@ -22,6 +22,11 @@
...
@@ -22,6 +22,11 @@
let
unknown_loc
=
Cil_datatype
.
Location
.
unknown
let
unknown_loc
=
Cil_datatype
.
Location
.
unknown
exception
BuildError
of
string
let
error
format
=
Format
.
kasprintf
(
fun
s
->
raise
(
BuildError
s
))
format
(* --- Types --- *)
(* --- Types --- *)
...
@@ -982,8 +987,6 @@ end
...
@@ -982,8 +987,6 @@ end
let
dkey
=
Kernel
.
register_category
"cil-builder"
let
dkey
=
Kernel
.
register_category
"cil-builder"
exception
WrongContext
of
string
module
Stateful
()
=
module
Stateful
()
=
struct
struct
include
Exp
include
Exp
...
@@ -1015,7 +1018,7 @@ struct
...
@@ -1015,7 +1018,7 @@ struct
let
build_instr_list
l
=
let
build_instr_list
l
=
let
rev_build_one
acc
=
function
let
rev_build_one
acc
=
function
|
Label
_
|
CilStmt
_
|
CilStmtkind
_
->
|
Label
_
|
CilStmt
_
|
CilStmtkind
_
->
raise
(
WrongContext
"not convertible to instr"
)
error
"the statement is not an instruction"
|
CilInstr
instr
->
instr
::
acc
|
CilInstr
instr
->
instr
::
acc
in
in
List
.
fold_left
rev_build_one
[]
l
List
.
fold_left
rev_build_one
[]
l
...
@@ -1064,7 +1067,7 @@ struct
...
@@ -1064,7 +1067,7 @@ struct
let
case_stmts
=
List
.
filter
contains_case
block
.
bstmts
in
let
case_stmts
=
List
.
filter
contains_case
block
.
bstmts
in
Cil_types
.
Switch
(
switch_exp
,
block
,
case_stmts
,
b
.
loc
)
Cil_types
.
Switch
(
switch_exp
,
block
,
case_stmts
,
b
.
loc
)
|
Function
_
->
|
Function
_
->
raise
(
WrongContext
"
not convertible to stmtkind"
)
error
"the function block is
not convertible to
Cil_types.
stmtkind"
(* State management *)
(* State management *)
...
@@ -1076,12 +1079,12 @@ struct
...
@@ -1076,12 +1079,12 @@ struct
let
set_owner
o
=
let
set_owner
o
=
if
Option
.
is_some
!
owner
then
if
Option
.
is_some
!
owner
then
raise
(
WrongContext
"already in a function"
)
;
error
"already in a function
context
"
;
owner
:=
Some
o
owner
:=
Some
o
let
get_owner
()
=
let
get_owner
()
=
match
!
owner
with
match
!
owner
with
|
None
->
raise
(
WrongContext
"function context not set"
)
|
None
->
error
"function context not set"
|
Some
fundec
->
fundec
|
Some
fundec
->
fundec
...
@@ -1101,15 +1104,15 @@ struct
...
@@ -1101,15 +1104,15 @@ struct
let
check_empty
()
=
let
check_empty
()
=
if
!
stack
<>
[]
then
if
!
stack
<>
[]
then
raise
(
WrongContext
"some contextes have not been closed
"
)
error
"some contextes have not been closed
: %t"
pretty_stack
!
stack
let
check_not_empty
()
=
let
check_not_empty
()
=
if
!
stack
=
[]
then
if
!
stack
=
[]
then
raise
(
WrongContext
"only a finish_* function can close all contextes"
)
error
"only a finish_* function can close all contextes"
let
top
()
=
let
top
()
=
match
!
stack
with
match
!
stack
with
|
[]
->
raise
(
WrongContext
"not in an opened context"
)
|
[]
->
error
"not in an opened context"
|
state
::
_
->
state
|
state
::
_
->
state
let
push
state
=
let
push
state
=
...
@@ -1123,7 +1126,7 @@ struct
...
@@ -1123,7 +1126,7 @@ struct
let
pop
()
=
let
pop
()
=
Kernel
.
debug
~
dkey
"pop from %t"
pretty_stack
;
Kernel
.
debug
~
dkey
"pop from %t"
pretty_stack
;
match
!
stack
with
match
!
stack
with
|
[]
->
raise
(
WrongContext
"not in an opened context"
)
|
[]
->
error
"not in an opened context"
|
hd
::
tail
->
|
hd
::
tail
->
stack
:=
tail
;
stack
:=
tail
;
hd
hd
...
@@ -1131,9 +1134,9 @@ struct
...
@@ -1131,9 +1134,9 @@ struct
let
finish
()
=
let
finish
()
=
reset_owner
()
;
reset_owner
()
;
match
!
stack
with
match
!
stack
with
|
[]
->
raise
(
WrongContext
"not in an opened context"
)
|
[]
->
error
"not in an opened context"
|
[
b
]
->
stack
:=
[]
;
b
|
[
b
]
->
stack
:=
[]
;
b
|
_
::
_
::
_
->
raise
(
WrongContext
"all contextes have not been closed"
)
|
_
::
_
::
_
->
error
"all contextes have not been closed"
let
append_stmt
b
s
=
let
append_stmt
b
s
=
b
.
stmts
<-
s
::
b
.
stmts
b
.
stmts
<-
s
::
b
.
stmts
...
@@ -1188,17 +1191,17 @@ struct
...
@@ -1188,17 +1191,17 @@ struct
let
extract_ifthen_block
b
=
let
extract_ifthen_block
b
=
match
b
.
scope_type
with
match
b
.
scope_type
with
|
IfThen
{
ifthen_exp
}
->
ifthen_exp
|
IfThen
{
ifthen_exp
}
->
ifthen_exp
|
_
->
raise
(
WrongContext
"not in an opened if-then-else context"
)
|
_
->
error
"not in an opened if-then-else context"
let
extract_switch_block
b
=
let
extract_switch_block
b
=
match
b
.
scope_type
with
match
b
.
scope_type
with
|
Switch
{
switch_exp
}
->
switch_exp
|
Switch
{
switch_exp
}
->
switch_exp
|
_
->
raise
(
WrongContext
"not in a opened switch context"
)
|
_
->
error
"not in a opened switch context"
let
extract_function_block
b
=
let
extract_function_block
b
=
match
b
.
scope_type
with
match
b
.
scope_type
with
|
Function
{
fundec
}
->
fundec
|
Function
{
fundec
}
->
fundec
|
_
->
raise
(
WrongContext
"not in a opened function context"
)
|
_
->
error
"not in a opened function context"
let
open_function
?
(
loc
=
current_loc
()
)
?
ghost
?
vorig_name
name
=
let
open_function
?
(
loc
=
current_loc
()
)
?
ghost
?
vorig_name
name
=
check_empty
()
;
check_empty
()
;
...
@@ -1242,7 +1245,7 @@ struct
...
@@ -1242,7 +1245,7 @@ struct
let
b
=
finish
()
in
let
b
=
finish
()
in
match
build_stmtkind
b
with
match
build_stmtkind
b
with
|
Cil_types
.
Block
b
->
b
|
Cil_types
.
Block
b
->
b
|
_
->
raise
(
WrongContext
"not in an opened simple block context"
)
|
_
->
error
"not in an opened simple block context"
let
finish_instr_list
?
scope
()
=
let
finish_instr_list
?
scope
()
=
let
b
=
finish
()
in
let
b
=
finish
()
in
...
@@ -1251,7 +1254,7 @@ struct
...
@@ -1251,7 +1254,7 @@ struct
|
Some
block
,
vars
->
|
Some
block
,
vars
->
block
.
Cil_types
.
blocals
<-
List
.
rev
vars
@
block
.
Cil_types
.
blocals
block
.
Cil_types
.
blocals
<-
List
.
rev
vars
@
block
.
Cil_types
.
blocals
|
None
,
_
::
_
->
|
None
,
_
::
_
->
raise
(
WrongContext
"a scope must be provided to insert local variables"
)
error
"a scope must be provided to insert local variables"
end
;
end
;
build_instr_list
b
.
stmts
build_instr_list
b
.
stmts
...
@@ -1281,7 +1284,7 @@ struct
...
@@ -1281,7 +1284,7 @@ struct
let
open
Cil_types
in
let
open
Cil_types
in
let
vi
=
fundec
.
svar
and
spec
=
fundec
.
sspec
in
let
vi
=
fundec
.
svar
and
spec
=
fundec
.
sspec
in
if
b
.
stmts
<>
[]
then
if
b
.
stmts
<>
[]
then
raise
(
WrongContext
"there must not be any built statements"
)
;
error
"there must not be any built statements"
;
vi
.
vdefined
<-
false
;
vi
.
vdefined
<-
false
;
vi
.
vghost
<-
b
.
ghost
;
vi
.
vghost
<-
b
.
ghost
;
if
register
then
begin
if
register
then
begin
...
...
This diff is collapsed.
Click to expand it.
src/kernel_services/ast_building/cil_builder.mli
+
1
−
1
View file @
31ca77be
...
@@ -287,7 +287,7 @@ end
...
@@ -287,7 +287,7 @@ end
(* --- Stateful builder --- *)
(* --- Stateful builder --- *)
exception
WrongContext
of
string
exception
BuildError
of
string
module
Stateful
()
:
module
Stateful
()
:
sig
sig
...
...
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