Anonymous Login Frama-C issues should now be submitted on Frama-C's GitLab
2021-03-06 03:34 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0002502Frama-CPlug-in > Evapublic2020-06-12 08:59
Reporterpuccetti2 
Assigned Tobuhler 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformMacOS XOSOS Version10.15.3
Product VersionFrama-C 19-Potassium 
Target VersionFixed in VersionFrama-C 21-Scandium 
Summary0002502: development version
DescriptionRunning EVA on the small example leads to a cash
Steps To Reproduceframa-c-gui max_array2.c -val
Additional Information
$ frama-c max_array2.c -val
[kernel] Parsing max_array2.c (with preprocessing)
[kernel:parser:decimal-float] max_array2.c:26: Warning: 
  Floating-point constant 4.6 is not represented exactly. Will use 0x1.2666666666666p2.
  (warn-once: no further messages from category 'parser:decimal-float' will be emitted)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
  
[eva:alarm] max_array2.c:28: Warning: 
  function max_array: precondition ∀ ℤ j;
                                     0 ≤ j < n ⇒ \valid_read(t + j) got status unknown.
[kernel] Current source was: max_array2.c:15
  The full backtrace is:
  Raised at file "src/plugins/value/legacy/eval_terms.ml", line 1264, characters 9-21
  Called from file "src/plugins/value/legacy/eval_terms.ml", line 1030, characters 13-41
  Called from file "src/plugins/value/legacy/eval_terms.ml", line 2127, characters 18-66
  Called from file "src/plugins/value/legacy/eval_terms.ml", line 2308, characters 4-20
  Called from file "src/plugins/value/domains/cvalue/cvalue_domain.ml", line 284, characters 10-49
  Called from file "src/plugins/value/engine/transfer_logic.ml", line 663, characters 25-61
  Called from file "list.ml", line 121, characters 24-34
  Called from file "src/plugins/value/engine/transfer_logic.ml", line 660, characters 10-488
  Called from file "list.ml", line 121, characters 24-34
  Called from file "src/plugins/value/engine/iterator.ml", line 377, characters 8-69
  Called from file "src/plugins/value/engine/iterator.ml", line 381, characters 17-61
  Called from file "src/plugins/value/engine/partition.ml", line 481, characters 29-34
  Called from file "list.ml", line 121, characters 24-34
  Called from file "src/plugins/value/engine/iterator.ml", line 469, characters 8-57
  Called from file "src/plugins/value/engine/iterator.ml", line 556, characters 12-45
  Called from file "list.ml", line 110, characters 12-15
  Called from file "src/plugins/value/engine/iterator.ml" (inlined), line 542, characters 4-31
  Called from file "src/plugins/value/engine/iterator.ml", line 604, characters 6-22
  Called from file "src/plugins/value/engine/iterator.ml", line 774, characters 20-39
  Called from file "src/plugins/value/engine/compute_functions.ml", line 210, characters 8-45
  Called from file "src/plugins/value/engine/compute_functions.ml", line 230, characters 26-36
  Called from file "src/plugins/value/engine/transfer_stmt.ml", line 307, characters 10-43
  Called from file "src/plugins/value/engine/transfer_stmt.ml", line 445, characters 22-60
  Called from file "src/plugins/value/engine/transfer_stmt.ml", line 749, characters 26-75
  Called from file "src/kernel_services/abstract_interp/bottom.ml" (inlined), line 31, characters 18-21
  Called from file "src/plugins/value/engine/transfer_stmt.ml", line 745, characters 10-447
  Called from file "list.ml", line 121, characters 24-34
  Called from file "src/plugins/value/engine/transfer_stmt.ml", line 760, characters 24-59
  Called from file "src/kernel_services/abstract_interp/bottom.ml" (inlined), line 31, characters 18-21
  Called from file "src/plugins/value/engine/transfer_stmt.ml", line 733, characters 6-1023
  Called from file "src/plugins/value/engine/iterator.ml", line 277, characters 6-47
  Called from file "src/plugins/value/engine/partition.ml", line 481, characters 29-34
  Called from file "list.ml", line 121, characters 24-34
  Called from file "src/plugins/value/engine/iterator.ml", line 430, characters 15-71
  Called from file "src/plugins/value/engine/iterator.ml", line 496, characters 18-35
  Called from file "list.ml", line 92, characters 20-23
  Called from file "src/plugins/value/engine/iterator.ml", line 498, characters 18-60
  Called from file "src/plugins/value/engine/iterator.ml", line 545, characters 13-31
  Called from file "list.ml", line 110, characters 12-15
  Called from file "src/plugins/value/engine/iterator.ml" (inlined), line 542, characters 4-31
  Called from file "src/plugins/value/engine/iterator.ml", line 604, characters 6-22
  Called from file "src/plugins/value/engine/iterator.ml", line 774, characters 20-39
  Called from file "src/plugins/value/engine/compute_functions.ml", line 210, characters 8-45
  Called from file "src/plugins/value/engine/compute_functions.ml", line 343, characters 25-75
  Called from file "src/libraries/project/state_builder.ml", line 994, characters 9-13
  Re-raised at file "src/libraries/project/state_builder.ml", line 1002, characters 9-18
  Called from file "src/plugins/value/register.ml", line 39, characters 46-66
  Called from file "queue.ml", line 121, characters 6-15
  Called from file "src/kernel_internals/runtime/boot.ml", line 36, characters 4-20
  Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 792, characters 2-9
  Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 822, characters 18-64
  Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 229, characters 4-8
  
  Unexpected error (File "src/plugins/value/legacy/eval_terms.ml", line 1264, characters 9-15: Assertion failed).
TagsNo tags attached.
Attached Files
  • c file icon max_array2.c (627 bytes) 2020-03-12 15:20 -
    #include "stdlib.h"
    #include "stdio.h"
    
    /*@ requires (n>0);
    	@ requires \valid(t);
    	@ requires \forall integer j; 0<=j<n ==> \valid_read (t+j);
    	@ ensures \result == \max (0, n-1, \lambda integer k; t[k]);
    	@*/
    double max_array(double* t, int n) {
        
        double m=0; 
        int i=0;
    		/*@ loop invariant 0 <= i < n && (m == \max(0,i,\lambda integer k; t[k]));
    			@ */
    		while (i<n) {
    			if (t[i] > m) { 
    				m = t[i]; 
    			};
    			i++;
        }
        return m;
    }
    
    int main ()
    {
        double t[6] = {3.5, 4.6, 1.8, 2.3, 9.1, 5.3};
        int a = 6;
        double res = max_array(t,a);
        fprintf(stdout,"Max value: %f", res);
    
        return 0;
    }
    
    c file icon max_array2.c (627 bytes) 2020-03-12 15:20 +

-Relationships
+Relationships

-Notes

~0006962

maroneze (administrator)

Thanks for the report.

Fixed in commit 4a4685f3 (Frama-C development branch).

The fixed version allows the user to realize that the loop invariant in the provided code is invalid, and should be:

  /*@ loop invariant 0 <= i <= n && (m == \max(0,i-1,\lambda integer k; t[k]));

~0006963

maroneze (administrator)

Fixed in commit 4a4685f3

~0006964

buhler (developer)

In ACSL, \max(i, j, f) is unspecified when i>j, so in the example, a loop invariant with \max(0,i-1,…) should never be proved.


Instead, you can use :
/*@ loop invariant 0 <= i <= n && (i == 0 || m == \max(0,i,\lambda integer k; t[k])); */


Or simply initialize the variable m to t[0].


In both cases, the example should be proved with Eva by using option -eva-auto-loop-unroll 10.


However, note that Eva precisely evaluates \max(i, j, f) only if i-j <= 10. Otherwise, imprecise over-approximations are made.
+Notes

-Issue History
Date Modified Username Field Change
2020-03-12 15:20 puccetti2 New Issue
2020-03-12 15:20 puccetti2 Status new => assigned
2020-03-12 15:20 puccetti2 Assigned To => buhler
2020-03-12 15:20 puccetti2 File Added: max_array2.c
2020-03-17 11:13 maroneze Additional Information Updated View Revisions
2020-03-17 13:59 maroneze Note Added: 0006962
2020-03-17 14:00 maroneze Note Added: 0006963
2020-03-17 14:00 maroneze Status assigned => resolved
2020-03-17 14:00 maroneze Fixed in Version => Frama-C GIT, precise the release id
2020-03-17 14:00 maroneze Resolution open => fixed
2020-03-17 14:47 buhler Note Added: 0006964
2020-06-12 08:59 signoles Fixed in Version Frama-C GIT, precise the release id => Frama-C 21-Scandium
2020-06-12 08:59 signoles Status resolved => closed
+Issue History