2020-12-04 23:39 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001003Frama-CPlug-in > jessiepublic2013-03-27 09:44
ReporterJochen 
Assigned Tocmarche 
PrioritynormalSeveritytweakReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C Nitrogen-20111001 
Target VersionFixed in VersionFrama-C Oxygen-20120901 
Summary0001003: conditional expression (?:) raises uncaught exception under why-2.30
DescriptionRunning "frama-c -cpp-command 'gcc -C -E -I.' -jessie '-jessie-why-opt=-exp goal' -no-unicode -jessie-atp simplify ftest.c" on the attached program yield a message:

Uncaught exception: Invalid_argument("equal: abstract value")

The reason seems to be the (?:) operator used in line 3.
I used frama-c Nitrogen-20111001 and why 2.30.
TagsNo tags attached.
Attached Files
  • c file icon ftest.c (51 bytes) 2011-10-27 15:49 -
    int ftest(int a) {
         return a == 4 ? 5 : a;
    }
    
    
    c file icon ftest.c (51 bytes) 2011-10-27 15:49 +
  • ? file icon typescript1 (6,180 bytes) 2011-11-10 15:20 -
    Script started on Thu Nov 10 14:16:34 2011
    ]0;-->~/devicesoft/Svn/device-soft/trunk/Framac/Nitrogen/Quarry/jochen     tora     jochentora:~/devicesoft/Svn/device-soft/trunk/Framac/Nitrogen/Quarry/jochen
    echo $OCAMLRUNPARAM 
    b
    ]0;-->~/devicesoft/Svn/device-soft/trunk/Framac/Nitrogen/Quarry/jochen     tora     jochentora:~/devicesoft/Svn/device-soft/trunk/Framac/Nitrogen/Quarry/jochen
    export OCAMLRUNPARAM
    ]0;-->~/devicesoft/Svn/device-soft/trunk/Framac/Nitrogen/Quarry/jochen     tora     jochentora:~/devicesoft/Svn/device-soft/trunk/Framac/Nitrogen/Quarry/jochen
    cat ftest1.c
    
    int ftest(int a) {
         return a == 4 ? 5 : a;
    }
    
    ]0;-->~/devicesoft/Svn/device-soft/trunk/Framac/Nitrogen/Quarry/jochen     tora     jochentora:~/devicesoft/Svn/device-soft/trunk/Framac/Nitrogen/Quarry/jochen
    frama-c.byte -cpp-command 'gcc -C -E -I.' -jessie '-jessie-why-opt=-exp goal' -no-unicode -jessie-atp simplify ftest1.c
    [kernel] preprocessing with "gcc -C -E -I.  -dD ftest1.c"
    [jessie] Starting Jessie translation
    [jessie] Producing Jessie files in subdir ftest1.jessie
    [jessie] File ftest1.jessie/ftest1.jc written.
    [jessie] File ftest1.jessie/ftest1.cloc written.
    [jessie] Calling Jessie tool in subdir ftest1.jessie
    Uncaught exception: Invalid_argument("equal: abstract value")
    [jessie] user error: Jessie subprocess failed:   jessie  -why-opt -split-user-conj  -v  -why-opt "-exp goal"     -locs ftest1.cloc ftest1.jc
    ]0;-->~/devicesoft/Svn/device-soft/trunk/Framac/Nitrogen/Quarry/jochen     tora     jochentora:~/devicesoft/Svn/device-soft/trunk/Framac/Nitrogen/Quarry/jochen
    cat ftest2.c
    
     int  ftest2(int n) { return 0 < n && n < 9; }
    
    ]0;-->~/devicesoft/Svn/device-soft/trunk/Framac/Nitrogen/Quarry/jochen     tora     jochentora:~/devicesoft/Svn/device-soft/trunk/Framac/Nitrogen/Quarry/jochen
    frama-c.byte -cpp-command 'gcc -C -E -I.' -jessie '-jessie-why-opt=-exp goal' -no-unicode -jessie-atp simplify ftest2.c
    [kernel] preprocessing with "gcc -C -E -I.  -dD ftest2.c"
    [jessie] Starting Jessie translation
    [jessie] Producing Jessie files in subdir ftest2.jessie
    [jessie] File ftest2.jessie/ftest2.jc written.
    [jessie] File ftest2.jessie/ftest2.cloc written.
    [jessie] Calling Jessie tool in subdir ftest2.jessie
    Uncaught exception: Invalid_argument("equal: abstract value")
    [jessie] user error: Jessie subprocess failed:   jessie  -why-opt -split-user-conj  -v  -why-opt "-exp goal"     -locs ftest2.cloc ftest2.jc
    ]0;-->~/devicesoft/Svn/device-soft/trunk/Framac/Nitrogen/Quarry/jochen     tora     jochentora:~/devicesoft/Svn/device-soft/trunk/Framac/Nitrogen/Quarry/jochen
    cat ftest3.c
    
    void ftest3(int n) { if (0 < n) n = 1; else n = 2; }
    
    ]0;-->~/devicesoft/Svn/device-soft/trunk/Framac/Nitrogen/Quarry/jochen     tora     jochentora:~/devicesoft/Svn/device-soft/trunk/Framac/Nitrogen/Quarry/jochen
    frama-c.byte -cpp-command 'gcc -C -E -I.' -jessie '-jessie-why-opt=-exp goal' -no-unicode -jessie-atp simplify ftest3.c
    [kernel] preprocessing with "gcc -C -E -I.  -dD ftest3.c"
    [jessie] Starting Jessie translation
    [jessie] Producing Jessie files in subdir ftest3.jessie
    [jessie] File ftest3.jessie/ftest3.jc written.
    [jessie] File ftest3.jessie/ftest3.cloc written.
    [jessie] Calling Jessie tool in subdir ftest3.jessie
    Uncaught exception: Invalid_argument("equal: abstract value")
    [jessie] user error: Jessie subprocess failed:   jessie  -why-opt -split-user-conj  -v  -why-opt "-exp goal"     -locs ftest3.cloc ftest3.jc
    ]0;-->~/devicesoft/Svn/device-soft/trunk/Framac/Nitrogen/Quarry/jochen     tora     jochentora:~/devicesoft/Svn/device-soft/trunk/Framac/Nitrogen/Quarry/jochen
    which frama-c
    /usr/local/bin/frama-c
    ]0;-->~/devicesoft/Svn/device-soft/trunk/Framac/Nitrogen/Quarry/jochen     tora     jochentora:~/devicesoft/Svn/device-soft/trunk/Framac/Nitrogen/Quarry/jochen
    which frama-c.byte
    /usr/local/bin/frama-c.byte
    ]0;-->~/devicesoft/Svn/device-soft/trunk/Framac/Nitrogen/Quarry/jochen     tora     jochentora:~/devicesoft/Svn/device-soft/trunk/Framac/Nitrogen/Quarry/jochen
    ll /usr/local/bin/frama-c*
    -rwxr-xr-x 1 root  7736753 Oct 28 13:00 /usr/local/bin/frama-c
    -rwxr-xr-x 1 root 31384093 Oct 28 13:00 /usr/local/bin/frama-c.byte
    ]0;-->~/devicesoft/Svn/device-soft/trunk/Framac/Nitrogen/Quarry/jochen     tora     jochentora:~/devicesoft/Svn/device-soft/trunk/Framac/Nitrogen/Quarry/jochen
    frama-c -version
    Version: Nitrogen-20111001
    Compilation date: Fri Oct 28 12:54:56 CEST 2011
    Share path: /usr/local/share/frama-c (may be overridden with FRAMAC_SHARE variable)
    Library path: /usr/local/lib/frama-c (may be overridden with FRAMAC_LIB variable)
    Plug-in paths: /usr/local/lib/frama-c/plugins (may be overridden with FRAMAC_PLUGIN variable)
    ]0;-->~/devicesoft/Svn/device-soft/trunk/Framac/Nitrogen/Quarry/jochen     tora     jochentora:~/devicesoft/Svn/device-soft/trunk/Framac/Nitrogen/Quarry/jochen
    frama-c.byte -version
    Version: Nitrogen-20111001
    Compilation date: Fri Oct 28 12:54:56 CEST 2011
    Share path: /usr/local/share/frama-c (may be overridden with FRAMAC_SHARE variable)
    Library path: /usr/local/lib/frama-c (may be overridden with FRAMAC_LIB variable)
    Plug-in paths: /usr/local/lib/frama-c/plugins (may be overridden with FRAMAC_PLUGIN variable)
    ]0;-->~/devicesoft/Svn/device-soft/trunk/Framac/Nitrogen/Quarry/jochen     tora     jochentora:~/devicesoft/Svn/device-soft/trunk/Framac/Nitrogen/Quarry/jochen
    why -version
    This is why version 2.30, compiled on Fri Oct 28 13:01:34 CEST 2011
    Copyright (c) 2002-2011 CNRS/INRIA/Univ Paris 11, team ProVal
    This is free software with ABSOLUTELY NO WARRANTY (use option -warranty)
    ]0;-->~/devicesoft/Svn/device-soft/trunk/Framac/Nitrogen/Quarry/jochen     tora     jochentora:~/devicesoft/Svn/device-soft/trunk/Framac/Nitrogen/Quarry/jochen
    
    Script done on Thu Nov 10 14:20:23 2011
    
    ? file icon typescript1 (6,180 bytes) 2011-11-10 15:20 +
  • ? file icon typescript2 (2,246 bytes) 2011-11-10 15:20 -
    Script started on Thu Nov 10 15:08:15 2011
    ]0;-->~/devicesoft/Svn/device-soft/trunk/Framac/Nitrogen/Quarry/jochen     tora     jochentora:~/devicesoft/Svn/device-soft/trunk/Framac/Nitrogen/Quarry/jochen
    cd ftest2.jessie
    ]0;-->~/devicesoft/Svn/device-soft/trunk/Framac/Nitrogen/Quarry/jochen/ftest2.jessie     tora     jochentora:~/devicesoft/Svn/device-soft/trunk/Framac/Nitrogen/Quarry/jochen/ftest2.jessie
    OCAMLRUNPARAM=b jessie -d -why-opt -split-user-conj -v -why-opt "-exp goal" -locs ftest2.cloc ftest2.jc
    
    AST AFTER PARSING:
    
    axiomatic Padding {
    
      logic type padding
      
    }
    
    type int8 = -128..127
    
    type int32 = -2147483648..2147483647
    
    tag charP = {
      int8 charM: 8;
    }
    
    type charP = [charP]
    
    tag voidP = {
    }
    
    type voidP = [voidP]
    
    int32 ftest2(int32 n)
    behavior default:
      ensures (C_4 : true);
    {  
       (var int32 tmp);
       
       {  (if (0 < n) then (if (n < 9) then (C_3 : (tmp = 1)) else (C_2 : (tmp = 0))) else 
          (C_1 : (tmp = 0)));
          
          (return tmp)
       }
    }
    
    Fatal error: exception Invalid_argument("equal: abstract value")
    ]0;-->~/devicesoft/Svn/device-soft/trunk/Framac/Nitrogen/Quarry/jochen/ftest2.jessie     tora     jochentora:~/devicesoft/Svn/device-soft/trunk/Framac/Nitrogen/Quarry/jochen/ftest2.jessie
    ll
    total 12
    -rw-r--r-- 1 jochen 669 Nov 10 14:57 ftest2.cloc
    -rw-r--r-- 1 jochen 573 Nov 10 14:57 ftest2.jc
    -rw-r--r-- 1 jochen 231 Nov 10 15:08 jessie.log
    ]0;-->~/devicesoft/Svn/device-soft/trunk/Framac/Nitrogen/Quarry/jochen/ftest2.jessie     tora     jochentora:~/devicesoft/Svn/device-soft/trunk/Framac/Nitrogen/Quarry/jochen/ftest2.jessie
    cat jessie.log
    WHYLIB is not set, using /usr/local/lib/why as default
    Parsing
    Normalization
    Typing logic labels
    Typing code
    Typing axiomatic Padding
    Typing logic type declaration padding
    Typing axiomatic Padding
    Typing tag charP
    Typing tag voidP
    ]0;-->~/devicesoft/Svn/device-soft/trunk/Framac/Nitrogen/Quarry/jochen/ftest2.jessie     tora     jochentora:~/devicesoft/Svn/device-soft/trunk/Framac/Nitrogen/Quarry/jochen/ftest2.jessie
    
    Script done on Thu Nov 10 15:08:57 2011
    
    ? file icon typescript2 (2,246 bytes) 2011-11-10 15:20 +
  • c file icon ftest3.c (197 bytes) 2011-11-18 14:53 -
    void ftest3(int n) {
        //@ assert \true;
        if (0 < n) {
    	//@ assert 0 < n;
    	n = 1;
    	//  assert \true;
        } else {
    	//@ assert n <= 0;
    	n = 2;
    	//  assert \true;
        }
        //@ assert n >= 1;
    }
    
    c file icon ftest3.c (197 bytes) 2011-11-18 14:53 +
  • txt file icon Output1003.txt (2,655 bytes) 2012-02-15 15:15 -
    Patch applied to jc_typing.ml: 
    
    let mintype loc t1 t2 =
      (* Patch: Following line shows what is really going on: *)
      Format.printf "mintype: Attempting to match %a vs. %a\n" print_type t1 print_type t2;
      try match t1,t2 with
        | JCTnative Tinteger, JCTnative Treal
    
        (* All pattern matches left as they are, removed from report for clarity *)
    
        | JCTpointer _, JCTpointer(JCtag(_, _::_), _, _) -> assert false
            (* TODO: parameterized type *)
        | _ -> raise Not_found
      with Not_found ->
        typing_error loc "incompatible types: %a and %a"
          print_type t1 print_type t2
     (* Patch: Validate the error indeed comes from here: *)
        | Invalid_argument("equal: abstract value") -> typing_error loc "Bug #1003 has bitten"
    
    
    Callstack from calling jessie on larger codebase - without the second patch/match for
    Invalid_argument in mintype:
    
      mintype: Attempting to match int32 vs. int32
      Fatal error: exception Invalid_argument("equal: abstract value")
      Raised by primitive operation at file "jc/jc_typing.ml", line 305, characters 11
      -16
      Called from file "jc/jc_typing.ml", line 2164, characters 20-77
      Called from file "list.ml", line 57, characters 20-23
      Called from file "jc/jc_typing.ml", line 2243, characters 18-32
      Called from file "list.ml", line 57, characters 20-23
      Called from file "jc/jc_typing.ml", line 2243, characters 18-32
      Called from file "jc/jc_typing.ml", line 2227, characters 18-41
      Called from file "list.ml", line 57, characters 20-23
      Called from file "jc/jc_typing.ml", line 2243, characters 18-32
      Called from file "jc/jc_typing.ml", line 2227, characters 18-41
      Called from file "list.ml", line 57, characters 20-23
      Called from file "jc/jc_typing.ml", line 2243, characters 18-32
      Called from file "jc/jc_pervasives.ml", line 46, characters 26-31
      Called from file "src/option_misc.ml", line 34, characters 51-56
      Called from file "jc/jc_typing.ml", line 3081, characters 20-95
      Called from file "jc/jc_typing.ml", line 3398, characters 9-52
      Called from file "list.ml", line 69, characters 12-15
      Called from file "jc/jc_typing.ml", line 3563, characters 2-40
      Called from file "jc/jc_main.ml", line 106, characters 4-27
      Called from file "jc/jc_main.ml", line 478, characters 27-34
    
    Result from calling jessie on ftest3.c (with second patch active - a stack trace
    is not provided even without the second patch):
    
      C:\Frama-C-Tests\test4.jessie>jessie.exe -why3ml -v -locs test4.cloc test4.jc
      File "test4.jc", line 38, characters 10-343: typing error: Bug #1003 has bitten
      mintype: Attempting to match int32 vs. int32
    
    txt file icon Output1003.txt (2,655 bytes) 2012-02-15 15:15 +

-Relationships
+Relationships

-Notes

~0002428

Jochen (reporter)

The same exception is raised also on the following program:

        int ftest2(int n) { return 0 < n && n < 9; }

And also on that one:

        void ftest3(int n) { if (0 < n) n = 1; else n = 2; }

~0002429

pascal (reporter)

If this is a regression in Nitrogen (is it?), this could be a consequence of switching to multiprecision integers in the AST for Nitrogen. In this case, the fix would be to change the = somewhere in the implementation to My_bigint.equal.

~0002433

cmarche (developer)


I can't reproduce that behavior. My guess is that it may occur only if an quite old version of Ocaml was used to compile the tools.

~0002453

pascal (reporter)

Following e-mails to the wrong person (that is, me), this issue is still open, and has been reproduced on a clean Linux installation. I also see others on the internet discussing this bug, most likely because it affects them.

Claude, I am guessing that you perhaps have OCaml 3.12.1, GMP and Zarith installed, and HAS_ZARITH defined to "yes". In this case, for you, (=) can be applied to big ints. This is one of the problem with Zarith: it makes (=) work (and makes it work correctly) between big ints.

The problem is that people who do not have Zarith, or do not have OCaml 3.12.1, still will see errors on applications of (=) to big ints.

Jochen, please try to substitute "frama-c.byte" to "frama-c" and see if you obtain a backtrace (please keep using "export OCAMLRUNPARAM=b". In fact, put it in your .profile, there is no reason not to want backtraces).

~0002463

Jochen (reporter)

I put "export OCAMLRUNPARAM=b" into my .profile and ran "frama-c.byte", as suggested by Pascal; however, I didn't obtain a backtrace (see file typescript1).

Frama-c.byte calls /usr/local/bin/jessie as a subprocess. I found out its args and env and called it again manyally, with an extra option "-d". This produced slightly more output (see file typescript2), but still no backtrace.

~0002477

Jochen (reporter)

While I gave up my attempts to produce a backtrace, I happened to find a new strange property: the error disappears if an assert-clause is inserted at the end of the then- or else-part, or both.

See the newly uploaded file ftest3.c. Put a "@" in line 6 or 10 to get it verified by Jessie(2.30) and Simplify.

None of the asserts in line 2,4,8,12 can cause this effect, even if they are weakened to \true. On the other hand, the asserts in line 6,10 work well also with formulas different from \true. In fact, the asserted formulas seem to have no influence.

~0002706

flecsim (reporter)

While attempting to circumvent issue 0001093, i triggered the same message, and in search for remedy i found this issue. I was able to retrieve a backtrace, but unfortunately i cannot supply the input (confidential).
However, i was able to trace this into jc_typing.mintype, where i added two patches in hope to find whats going on. The problem arised on (attempt to) evaluating "mintype _ int32 int32" for whatever reason.

Patch and output have been attached as "Output1003.txt". Maybe this helps in nailing down the problem.

~0002752

flecsim (reporter)

For me, the error disappeared on patching the definition of expr in jc_typing.ml, lines 2156-2167:
Before:

  | JCTnative Tboolean ->
    let te2,te3 =
      if same_type_no_coercion te2#typ te3#typ then
        te2,te3
      else
        unit_expr te2, unit_expr te3
    in
      let t = mintype e#pos
                      te2#typ
                      te3#typ
      in
        t, te2#region, JCEif(te1, te2, te3)

After:

  | JCTnative Tboolean ->
    let te2,te3 = unit_expr te2, unit_expr te3
    in
      let t = mintype e#pos
                      te2#typ
                      te3#typ
      in
        t, te2#region, JCEif(te1, te2, te3)

I am not sure whether this change may cause malfunction of Jessie, but i had quite some
"abstract value" errors collected among various projects. As none of them held up against
the patch, chances are the problem is located in that area of code.

~0003094

yakobowski (manager)

I have never been able to reproduce this bug myself, but there is something suspicious in the body of same_type_no_coercion

let same_type_no_coercion t1 t2 =
  match t1,t2 with
    | JCTnative t1, JCTnative t2 -> t1=t2
    | JCTenum ei1, JCTenum ei2 -> ei1.jc_enum_info_name = ei2.jc_enum_info_name
    | JCTlogic s1, JCTlogic s2 -> (* ?? *) s1=s2 (* ?? *)
[...]

Can you try again with this definition instead?

let rec same_type_no_coercion t1 t2 =
  match t1,t2 with
    | JCTnative t1, JCTnative t2 -> t1=t2
    | JCTenum ei1, JCTenum ei2 -> ei1.jc_enum_info_name = ei2.jc_enum_info_name
    | JCTlogic (name1, args1), JCTlogic (name2, args2) ->
        name1=name2 && List.for_all2 same_type_no_coercion args1 args2
(* following identical *)

~0003191

cmarche (developer)

I applied the modifications suggested by Boris into the SVN. No tests in the regression suite is affected, so I guees it is hamless ans the issue can be assumed as resolved.

~0003780

signoles (manager)

Fixed in Frama-C Oxygen + Why 2.32.
+Notes

-Issue History
Date Modified Username Field Change
2011-10-27 15:49 Jochen New Issue
2011-10-27 15:49 Jochen Status new => assigned
2011-10-27 15:49 Jochen Assigned To => cmarche
2011-10-27 15:49 Jochen File Added: ftest.c
2011-10-27 16:08 Jochen Note Added: 0002428
2011-10-27 18:03 pascal Note Added: 0002429
2011-10-28 07:05 cmarche Note Added: 0002433
2011-10-28 07:05 cmarche Status assigned => closed
2011-10-28 07:05 cmarche Resolution open => unable to reproduce
2011-11-07 01:30 pascal Note Added: 0002453
2011-11-07 01:30 pascal Status closed => feedback
2011-11-07 01:30 pascal Resolution unable to reproduce => reopened
2011-11-10 15:20 Jochen File Added: typescript1
2011-11-10 15:20 Jochen File Added: typescript2
2011-11-10 15:24 Jochen Note Added: 0002463
2011-11-18 14:53 Jochen File Added: ftest3.c
2011-11-18 15:02 Jochen Note Added: 0002477
2012-02-15 15:15 flecsim File Added: Output1003.txt
2012-02-15 15:16 flecsim Note Added: 0002706
2012-03-06 11:34 flecsim Note Added: 0002752
2012-06-10 14:06 yakobowski Note Added: 0003094
2012-06-22 18:01 cmarche Note Added: 0003191
2012-06-22 18:02 cmarche Status feedback => resolved
2012-06-22 18:02 cmarche Resolution reopened => fixed
2013-03-27 09:43 signoles Note Added: 0003780
2013-03-27 09:44 signoles Fixed in Version => Frama-C Oxygen-20120901
2013-03-27 09:44 signoles Status resolved => closed
+Issue History