2021-01-15 15:31 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001132Frama-CKernelpublic2014-02-12 16:59
ReporterAnne 
Assigned Tosignoles 
PrioritynormalSeverityminorReproducibilityhave not tried
StatusclosedResolutionfixed 
Product Version 
Target VersionFixed in VersionFrama-C Oxygen-20120901 
Summary0001132: -cpp-extra-args option should be a list
DescriptionThe "-cpp-extra-args" option is a StringSet option. It seems to me that is should better be a list since the order might be important...
Additional InformationWith the following script:
=============================================
let main () =
  Kernel.CppExtraArgs.add "-Ilib1";
  Kernel.CppExtraArgs.add "-Ilib2";
  Kernel.Files.set [ "tests/test.c" ];
  ()

let main : unit -> unit =
  Dynamic.register ~plugin:"Frama_c_journal" "main"
    (Datatype.func Datatype.unit Datatype.unit)
    ~journalize:false main
let () = Cmdline.run_after_loading_stage main; Cmdline.is_going_to_load ()
=============================================

You always get :
[kernel] preprocessing with "gcc -C -E -I. -Ilib2 -Ilib1 tests/test.c"
whatever the order of the [Kernel.CppExtraArgs.add] commands is.
TagsNo tags attached.
Attached Files

-Relationships
+Relationships

-Notes

~0002799

Anne (reporter)

Of course, a workaround is to do :
  Kernel.CppExtraArgs.add "-Ilib1 -Ilib2";

~0002801

signoles (manager)

Last edited: 2012-03-26 10:21

Done. Note however that the order of -llib and -llib2 in the Frama-C command line below is yet not specified since the order in which command line options are parsed (without -then) remains unspecified.

$ frama-c foo.c -cpp-extra-args="-llib1" -cpp-extra-args="-llib2"

~0004712

signoles (manager)

Fix committed to stable/neon branch.
+Notes

-Issue History
Date Modified Username Field Change
2012-03-23 10:16 Anne New Issue
2012-03-23 10:19 Anne Note Added: 0002799
2012-03-26 09:48 signoles Status new => assigned
2012-03-26 09:48 signoles Assigned To => signoles
2012-03-26 09:53 svn
2012-03-26 09:53 svn Status assigned => resolved
2012-03-26 09:53 svn Resolution open => fixed
2012-03-26 09:57 signoles Note Added: 0002801
2012-03-26 10:21 signoles Note Edited: 0002801
2012-09-19 17:15 signoles Fixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16 signoles Status resolved => closed
2013-12-19 01:12 signoles Source_changeset_attached => framac master 44d1276b
2014-02-12 16:54 signoles Source_changeset_attached => framac stable/neon 44d1276b
2014-02-12 16:59 signoles Note Added: 0004712
2014-02-12 16:59 signoles Status closed => resolved
+Issue History