SYSTEM WARNING: 'session_name(): Cannot change session name when session is active' in '/home/gitlab-www/dokuwiki/inc/init.php' line 231

SYSTEM WARNING: 'session_set_cookie_params(): Cannot change session cookie parameters when session is active' in '/home/gitlab-www/dokuwiki/inc/init.php' line 232

mantis:frama-c:issue:731 [Frama-C]

User Tools

  • Logged in as: anonymous (anonymous)
  • Log Out

Site Tools


mantis:frama-c:issue:731

The following script does what is suggested in note 1519 of Issue 731. Namely, it detects pure prototypes whose signature does not name its arguments and give them the names x_0, x_1, …). This has an impact on generated assigns clauses for these prototypes. The code should work with the various brands of Frama-C Carbon but is largely untested. Use it at your own risk!

name_args.ml
open Cil_types
open Cil
 
(* Just adds name to the arguments of prototypes that do not have any.
   Frama-C's kernel will take care of propagating the information where
   necessary
*)
class name_args proj =
object
  inherit Visitor.frama_c_copy proj
  method vglob_aux g =
    match g with
        GVarDecl (s,v,l) when Cil.isFunctionType v.vtype ->
          if Kernel_function.is_definition (Globals.Functions.get v) then 
            SkipChildren
          else begin
            match Cil.unrollType v.vtype with
              | TFun(rt,(Some (("",_,_)::_ as args)),vargs,attrs) ->
                let idx = ref 0 in
                let args = 
                  List.map 
                    (fun (_,t,attr) -> 
                      let name = "x_" ^ string_of_int !idx in
                      incr idx; (name,t,attr))
                    args
                in
                let newt = TFun (rt,Some args,vargs,attrs) in
                v.vtype <- newt;
                Cil.setFormalsDecl v newt;
                ChangeDoChildrenPost([GVarDecl(s,v,l)],fun x -> x)
              | TFun _ -> SkipChildren
              | _ -> Cilmsg.fatal "should be a function type"
          end
      | _  -> SkipChildren
end
 
let name_args _ =
  (* create a new project to host the normalized code. *)
  let proj = 
    File.create_project_from_visitor 
      "normalize decls" (fun proj -> new name_args proj) 
  in
  (* Be sure to copy the command-line options to the new project, i.e.
     everything other than the AST and the built-in functions of CIL.
   *)
  let selection = 
    State_selection.Static.diff 
      State_selection.full 
      (State_selection.Static.with_dependencies Ast.self) 
  in
  let selection = 
    State_selection.Static.diff selection 
      (State_selection.Static.with_dependencies Builtin_functions.self) 
  in
  Project.copy ~selection proj;
  Project.set_current proj
 
(* We do the transformation right after Frama-C has set the options and the 
   source file names. The call to create_project_from_visitor will automatically
   trigger the parsing and standard normalization phase.
 *)
let () = Cmdline.run_after_setting_files name_args

Use it like this:

frama-c -load-script name_args.ml <other options> <source files>
mantis/frama-c/issue/731.txt · Last modified: 2011/02/20 19:33 by virgile