I have implemented the example code in chapter 4.17.7 in the Developer Manual.
The example is a copy visitor that adds an assertion for each division in the program, stating that the divisor is not zero.
The code is as follows:
open Cil_types
open Cil
module M = Plugin.Register
let syntax_alarm =
Emitter.create "Syntactic check" [ Emitter.Code_annot ] ~correctness:[]
~tuning:[]
class non_zero_divisor prj =
object (self)
inherit Visitor.generic_frama_c_visitor (Visitor_behavior.copy prj)
method! vexpr e =
match e.enode with
| BinOp ((Div | Mod), _, denom, _) ->
let logic_denom = Logic_utils.expr_to_term ~coerce:false denom in
let assertion = Logic_const.prel (Rneq, logic_denom, Cil.lzero ()) in
let stmt =
match self#current_kinstr with
| Kglobal -> assert false
| Kstmt s -> s
in
let kf = Option.get self#current_kf in
let new_stmt = Visitor_behavior.Get.stmt self#behavior stmt in
Options.Self.result "NewStmt: %a" Printer.pp_stmt new_stmt;
let new_kf = Visitor_behavior.Get.kernel_function self#behavior kf in
Queue.add
(fun () ->
Annotations.add_assert syntax_alarm ~kf:new_kf new_stmt assertion)
self#get_filling_actions;
DoChildren
| _ -> DoChildren
end
let execute () =
ignore
(File.create_project_from_visitor "syntactic check" (new non_zero_divisor))
When I apply the plugin on a C source code that contains a division operation I get the expected annotation in the output.
The problem is however, when I write a test for this plugin the test fails with an error stating that the logic variable in the generated annotation is not declared.
The test code that I am using is:
/* run.config
OPT: -autoload-plugins -sandbox
*/
void main() {
int a, b, c;
a = 4;
b = 2;
c = a/b;
}
and the output that I get when I run the test is:
...
[kernel] tests/s1/test.c:9: Failure:
[AST Integrity Check]
AST of syntactic check
logic variable b (25) is not declared
[kernel] Current source was: tests/s1/test.c:5
The full backtrace is:
Raised at Project.on in file "src/libraries/project/project.ml", line 405, characters 59-66
Called from File.init_project_from_visitor in file "src/kernel_services/ast_queries/file.ml", line 1818, characters 4-64
Called from File.create_project_from_visitor in file "src/kernel_services/ast_queries/file.ml", line 1842, characters 2-43
Called from Sandbox_visitor.execute in file "sandbox_visitor.ml", line 37, characters 4-79
Called from Stdlib__Queue.iter.iter in file "queue.ml", line 121, characters 6-15
Called from Boot.play_analysis in file "src/kernel_internals/runtime/boot.ml", line 36, characters 4-20
Called from Cmdline.play_in_toplevel_one_shot in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 846, characters 2-9
Called from Cmdline.play_in_toplevel in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 876, characters 18-64
Called from Cmdline.catch_toplevel_run in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 235, characters 4-8
Frama-C aborted: internal error.
Please report as 'crash' at https://git.frama-c.com/pub/frama-c/issues
Your Frama-C version is 24.0 (Chromium).
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
https://git.frama-c.com/pub/frama-c/-/wikis/Guidelines-for-reporting-bugs
I wonder why am I getting this error and how to solve this problem. Thanks!
Indeed, there is an issue in the example of the manual you are referring to. It manifests itself in your setting because when using ptests, the option -check gets automatically added to frama-c's command line in order to ensure that incoherence in the AST gets discovered sooner than later.
The bulk of the issue is that, while the visitor takes care of registering the annotation with the new statement of the new kernel function in the new project, it does not attempt to ensure that the logic_denom term refers to variables in the new project (and as a matter of fact it doesn't). Basically, we have to copy denom and update use of varinfo in order to use their copy in the new project, i.e. adding
let denom = Visitor.visitFramacExpr self#frama_c_plain_copy denom in
before translating denom into logic_denom in the code above. frama_c_plain_copy is a special method of the visitor that is a simple copy visitor (it copies each node it encounters) which shares its correspondance tables with self, so that denom will indeed be a copy of the original expression with references to varinfo in the new project.
For what it's worth, here is a standalone script which solves the issue:
open Cil_types
open Cil
let syntax_alarm =
Emitter.create "Syntactic check" [ Emitter.Code_annot ] ~correctness:[]
~tuning:[]
class non_zero_divisor prj =
object (self)
inherit Visitor.generic_frama_c_visitor (Visitor_behavior.copy prj)
method! vexpr e =
match e.enode with
| BinOp ((Div | Mod), _, denom, _) ->
let denom = Visitor.visitFramacExpr self#frama_c_plain_copy denom in
let logic_denom = Logic_utils.expr_to_term ~coerce:false denom in
let assertion = Logic_const.prel (Rneq, logic_denom, Cil.lzero ()) in
let stmt =
match self#current_kinstr with
| Kglobal -> assert false
| Kstmt s -> s
in
let kf = Option.get self#current_kf in
let new_stmt = Visitor_behavior.Get.stmt self#behavior stmt in
Kernel.result "NewStmt: %a" Printer.pp_stmt new_stmt;
let new_kf = Visitor_behavior.Get.kernel_function self#behavior kf in
Queue.add
(fun () ->
Annotations.add_assert syntax_alarm ~kf:new_kf new_stmt assertion)
self#get_filling_actions;
DoChildren
| _ -> DoChildren
end
let execute () =
ignore
(File.create_project_from_visitor "syntactic check" (new non_zero_divisor))
let () = Db.Main.extend execute
if it is in script_example.ml, and test.c is your example C file, then
frama-c -check -load-script script_example.ml test.c -then-last -print gives the following output (tested with Frama-C 25.0):
[kernel] Parsing test.c (with preprocessing)
[kernel] NewStmt: c = a / b;
[kernel] NewStmt: /*@ assert b ≢ 0; */
c = a / b;
/* Generated by Frama-C */
void main(void)
{
int a;
int b;
int c;
a = 4;
b = 2;
/*@ assert b ≢ 0; */
c = a / b;
return;
}