Commit 82a4855d authored by Julien Signoles's avatar Julien Signoles
Browse files

ready to write the visitor

parent a1f1dfd3
......@@ -32,7 +32,7 @@ PLUGIN_DIR ?=.
PLUGIN_ENABLE:=@ENABLE_E_ACSL@
PLUGIN_DYNAMIC:=@DYNAMIC_E_ACSL@
PLUGIN_NAME:=E_ACSL
PLUGIN_CMO:= options main
PLUGIN_CMO:= options visit main
PLUGIN_HAS_MLI:=yes
PLUGIN_DISTRIBUTED:=no
PLUGIN_DISTRIB_EXTERNAL:= Makefile.in configure.ac configure
......
......@@ -19,7 +19,66 @@
(* *)
(**************************************************************************)
let main () = ()
let check () =
try
ignore (Visit.do_visit false);
true
with Visit.Typing_error s ->
Options.error "%s" s;
false
let check =
Dynamic.register
~plugin:"e-acsl"
~journalize:true
"check"
(Datatype.func Datatype.unit Datatype.bool)
check
let fail_check () =
try ignore (Visit.do_visit false)
with Visit.Typing_error s -> Options.abort "%s" s
let fail_check =
Dynamic.register
~plugin:"e-acsl"
~journalize:true
"fail_check"
(Datatype.func Datatype.unit Datatype.unit)
fail_check
module Resulting_projects =
State_builder.Hashtbl
(Datatype.String.Hashtbl)
(Project.Datatype)
(struct
let name = "E-ACSL resulting projects"
let size = 7
let kind = `Correctness
let dependencies = [ Ast.self ]
end)
let generate_code =
Resulting_projects.memo
(fun name ->
try
let visit prj = Visit.do_visit ~prj true in
File.create_project_from_visitor name visit
with Visit.Typing_error s ->
Options.abort "%s" s)
let generate_code =
Dynamic.register
~plugin:"e-acsl"
~journalize:true
"generate_code"
(Datatype.func Datatype.string Project.ty)
generate_code
let main () =
let s = Options.Project_name.get () in
if s = "" then begin if Options.Check.get () then fail_check () end
else ignore (generate_code s)
let () = Db.Main.extend main
......
......@@ -28,6 +28,24 @@ assertion checker generator"
end)
include P
module Check =
False
(struct
let option_name = "-e-acsl-check"
let help = "only perform E-ACSL type checking"
let kind = `Correctness
end)
module Project_name =
EmptyString
(struct
let option_name = "-e-acsl-runtime"
let help = "generate a new project <prj> from the C program where E-ACSL \
code is transformed to C code for runtime assertion checking"
let kind = `Correctness
let arg_name = "prj"
end)
(*
Local Variables:
compile-command: "make"
......
......@@ -23,6 +23,9 @@ open Plugin
include S (** implementation of Log.S for E-ACSL *)
module Check: BOOL
module Project_name: STRING
(*
Local Variables:
compile-command: "make"
......
(**************************************************************************)
(* *)
(* This file is part of Frama-C. *)
(* *)
(* Copyright (C) 2007-2010 *)
(* CEA (Commissariat à l'Énergie Atomique) *)
(* *)
(* you can redistribute it and/or modify it under the terms of the GNU *)
(* Lesser General Public License as published by the Free Software *)
(* Foundation, version 2.1. *)
(* *)
(* It is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
(* GNU Lesser General Public License for more details. *)
(* *)
(* See the GNU Lesser General Public License version 2.1 *)
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(* *)
(**************************************************************************)
exception Typing_error of string
let do_visit ?(prj=Project.current ()) _generate =
(* let _p = prj in
assert false*) new Visitor.generic_frama_c_visitor prj (Cil.copy_visit ())
(*
Local Variables:
compile-command: "make"
End:
*)
(**************************************************************************)
(* *)
(* This file is part of Frama-C. *)
(* *)
(* Copyright (C) 2007-2010 *)
(* CEA (Commissariat à l'Énergie Atomique) *)
(* *)
(* you can redistribute it and/or modify it under the terms of the GNU *)
(* Lesser General Public License as published by the Free Software *)
(* Foundation, version 2.1. *)
(* *)
(* It is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
(* GNU Lesser General Public License for more details. *)
(* *)
(* See the GNU Lesser General Public License version 2.1 *)
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(* *)
(**************************************************************************)
exception Typing_error of string
val do_visit: ?prj:Project.t -> bool -> Visitor.frama_c_visitor
(*
Local Variables:
compile-command: "make"
End:
*)
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment