Support for function bodies #212
Conversation
| begin | ||
| Inc (My_P); | ||
| -- Will fail: symex does not see the value | ||
| pragma Assert (My_P = 50); |
There was a problem hiding this comment.
With this one I'm confused. Is this supposed to happen or not? Because I'd think after Inc (My_P) My_P would be 5, not 50?
There was a problem hiding this comment.
Perhaps the name for Inc is inappropriate. The subprogram actually adds a number based on the variable Var in the constant_decs package. Using the value that Var is initialised with, Inc adds 46 to its parameter. I think a more usual scenario that I think we should test is when a private type and deferred constant is used (as in the test below.
| @@ -0,0 +1,7 @@ | |||
| with Deferred_Const; use Deferred_Const; | |||
There was a problem hiding this comment.
I am not sure what this test is checking. Originally I provide a test program called use_deferred_const
with Deferred_Const; use Deferred_Const;
procedure Use_Deferred_Const is
No_Use : Priv := Def_Const;
begin
Inc (No_Use);
end Use_Deferred_Const;
If we add another priv constant to the package Deferred_Const as below:
package Deferred_Const is
type Priv is private;
Def_Const : constant Priv;
Def_Const_Plus_1 : constant Priv;
procedure Inc (P : in out Priv);
private
type Priv is range 1 .. 10;
Def_Const : constant Priv := 1;
Def_Const_Plus_1 := Def_Const + 1;
end Deferred_Const;
Then in Use_Deferred_Constant after the call to Inc we could place the
pragma Assert (No_Use = Def_Const_Plus_1);
Which should succeed.
There was a problem hiding this comment.
I haven't added the test, I just wanted it to reach symex. This way the the range-check for Def_Const is included in the verification. Even if we don't actually refer to anything from the package.
| procedure Test is | ||
| My_Rec : Partial_Dec := (A=>1); | ||
| begin | ||
| P(My_Rec); |
There was a problem hiding this comment.
What's P? Inc?
There was a problem hiding this comment.
P is just an increment routine. Perhaps better to rename. In retrospect I need not have made the test for an incomplete type declaration in a package I could have easily written:
procedure New_Incomlete_Dec is
type Partial_Dec;
procedure Inc (X : in out Partial_Dec);
type Partial_Dec is record
A : Integer;
end record;
procedure Inc (X : in out Partial_Dec) is
begin
X.A := X.A + 1;
end Inc;
V : Partial_Dec := (A => 19);
begin
Inc (V);
pragma Assert (V.A = 20);
end New_Incomlete_Dec;
|
|
||
|
|
||
| def process(debug, file, cbmcargs): | ||
| def process_gnat2goto(debug, file, not_main): |
There was a problem hiding this comment.
⛏️ I always get confused with 'not_' boolean flags, I'd flip it around and call this is_main and then do the negation when you ask for it. Alternatively, just use the name of the option, i.e. no_cprover_start.
| # Run(["cbmc", jsout, "--show-symbol-table"], output=symtab) | ||
| # Run(["cbmc", jsout, "--show-goto-functions"], output=gotoprog) | ||
| cmdline = ["cbmc", jsout] | ||
| out = unit + ".out" |
There was a problem hiding this comment.
This is pretty confusing now. You're just using the name of the last file as out?
There was a problem hiding this comment.
I guess I was. What about TEST_NAME instead of unit here?
| """Call gnat2goto (and cbmc) on all *.adb files from the current directory | ||
| PARAMETERS | ||
| none: yet |
There was a problem hiding this comment.
This docstring is lying about the parameters of this function.
| return "" | ||
| out = process_cbmc(debug, ada_body_files(), cbmcargs) | ||
| if debug: | ||
| print('<<< DEBUG ' + file + ' >>>') |
There was a problem hiding this comment.
Debug output (I'm guessing this'll go away once the draft phase is done)
There was a problem hiding this comment.
I did not add it, but I can remove it. Done.
| print('<<< END DEBUG ' + file + ' >>>') | ||
| print(filter_cbmc_output(out)) | ||
| gnat2goto_success = process_gnat2goto(debug, file, main != "" and file != main) | ||
| if gnat2goto_success == False: |
There was a problem hiding this comment.
why not just if not process_gnat2goto(...) instead?
There was a problem hiding this comment.
So that's the syntax, ok.
| if not gnat2goto_success: | ||
| return "" | ||
| out = process_cbmc(debug, ada_body_files(), cbmcargs) | ||
| if debug: |
There was a problem hiding this comment.
Shame on me, I didn't realise this was controlled through a flag. Maybe this shouldn't be removed after all, sorry
|
@xbauch Now that merging symtabs is supported can this be un-drafted? |
xbauch
force-pushed
the
feature/function-bodies
branch
from
12b445e to
2c9ebfb
Compare
To contain a callable and reach symex.
To contain callable and reach symex.
Since we can see the function body.
Absolute, op_or, and op_and. No functional change.
With a failing assertion.
And a succeeding assertion.
And a succeeding assertion.
This one always had an assertion.
We will decide if start should be added.
There is no reason for, e.g. packages to contain it.
So that we can say which Ada body contains the entry.
Change the py script to call gnat2goto separately on all ada bodies but then CBMC only once on all the json files. Also pass the no-cprover-start option if the main-file is specified in the prove argument.
We just have to specify which contains the entry.
xbauch
force-pushed
the
feature/function-bodies
branch
from
2c9ebfb to
50bd518
Compare
Make function names more descriptive and add callable to private_type_dec_array.
xbauch
force-pushed
the
feature/function-bodies
branch
from
50bd518 to
c9b7583
Compare
5 participants
1: allow calling function from packages.
2: allow linking two subprogram bodies.
Some tests needed to be changed as well as the py script calling them. This won't work until CBMC supports resolving conflicting JSON symtabs (or we stop gnat2goto producing them).