2021-01-27 10:57 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001309Frama-CKernel > ACSL implementationpublic2014-02-12 16:58
Reportersignoles 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
Product Version 
Target VersionFixed in VersionFrama-C Fluorine-20130401 
Summary0001309: Incorrect typing of term conditional over floats
Descriptionvoid foo(int c) {
  float f = 1.0;
  /*@ assert 0.0 <= (c ? f : 2.0); */
}

In this example, both terms f and 2.0 in the conditional must get type Real. That is not the case. You can see that by running the attached script on this file:
frama-c -load-script test.ml test.i
IF ????? float : ?
TagsNo tags attached.
Attached Files
  • ? file icon test.ml (440 bytes) 2012-11-19 16:51 -
    open Cil_types
    
    let main () =
      let c = object
        inherit Visitor.frama_c_inplace
        method vterm t =
          match t.term_node with
        | Tif(t1, t2, t3) ->
          Kernel.feedback "IF %a? %a : %a" 
    	Cil.d_logic_type t1.term_type
    	Cil.d_logic_type t2.term_type
    	Cil.d_logic_type t3.term_type;
          Cil.SkipChildren
        | _ ->
          Cil.DoChildren
      end
      in
      Visitor.visitFramacFileSameGlobals c (Ast.get ())
    
    let () = Db.Main.extend main
    
    ? file icon test.ml (440 bytes) 2012-11-19 16:51 +

-Relationships
+Relationships

-Notes

~0004607

Fix committed to stable/neon branch.
+Notes

-Issue History
Date Modified Username Field Change
2012-11-19 16:51 signoles New Issue
2012-11-19 16:51 signoles Status new => assigned
2012-11-19 16:51 signoles Assigned To => virgile
2012-11-19 16:51 signoles File Added: test.ml
2012-11-23 17:28 svn
2012-11-23 17:28 svn Status assigned => resolved
2012-11-23 17:28 svn Resolution open => fixed
2013-04-19 11:05 signoles Fixed in Version => Frama-C Fluorine
2013-04-19 11:05 signoles Status resolved => closed
2013-12-19 01:11 Source_changeset_attached => framac master 2e4bce9f
2014-02-12 16:53 Source_changeset_attached => framac stable/neon 2e4bce9f
2014-02-12 16:58 Note Added: 0004607
2014-02-12 16:58 Status closed => resolved
+Issue History