Skip to content

GitLab

  • Menu
Projects Groups Snippets
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • F frama-c
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 209
    • Issues 209
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 0
    • Merge requests 0
  • Deployments
    • Deployments
    • Releases
  • Monitor
    • Monitor
    • Incidents
  • Packages & Registries
    • Packages & Registries
    • Container Registry
  • Analytics
    • Analytics
    • Value stream
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #2563

Closed
Open
Created Jun 09, 2021 by Karine EM@karineek

Frama-C crashed with an unexpected error Abstract_interp.Error_Bottom

Steps to reproduce the issue

I ran frama-c with these parameters:

frama-c -eva -slevel 100 -plevel 255 -eva-precision 5 -val-warn-undefined-pointer-comparison pointer -no-val-alloc-returns-null -warn-signed-overflow -val -no-val-show-progress -machdep x86_64 4ee67af5850fa1e85ef52301e74c7093eba28573.c

and 4ee67af5850fa1e85ef52301e74c7093eba28573.c is the following program:

__attribute__((noinline)) int
f (int a, int b, int d)
{
  int r = 8;
  
  b += d + 42 -((short)((((int)(b)) %((int)(d)))))-((short)((((int)(b)) >>((int)(b))))) + 42 -((short)((((int)(b)) %((int)(d + 42 -((short)((((int)(b)) %((int)(d)))))-((short)((((int)(b)) >>((int)(b))))))))))-((short)((((int)(b)) >>((int)(b)))));
 
  r = b - d + 42 +((long)((((double)(r)) -((double)(r)))))-((int)((((double)(b - d)) -((double)(d)))))-((long)((((int)(b - d)) ^((int)(d)))))+((int)((((double)(b - d)) *((double)(b)))))-((int)((((int)(d)) >>((int)(b - d)))))-((short)((((int)(b)) >>((int)(r)))))-((int)((((int)(b - d)) >>((int)(b)))))+((long)((((int)(d)) &((int)(b - d))))) + 42 +((long)((((double)(r)) -((double)(r)))))-((int)((((int)(b - d + 42 +((long)((((double)(r)) -((double)(r)))))-((int)((((double)(b - d)) -((double)(d)))))-((long)((((int)(b - d)) ^((int)(d)))))+((int)((((double)(b - d)) *((double)(b)))))-((int)((((int)(d)) >>((int)(b - d)))))-((short)((((int)(b)) >>((int)(r)))))-((int)((((int)(b - d)) >>((int)(b)))))+((long)((((int)(d)) &((int)(b - d))))))) %((int)(b - d + 42 +((long)((((double)(r)) -((double)(r)))))-((int)((((double)(b - d)) -((double)(d)))))-((long)((((int)(b - d)) ^((int)(d)))))+((int)((((double)(b - d)) *((double)(b)))))-((int)((((int)(d)) >>((int)(b - d)))))-((short)((((int)(b)) >>((int)(r)))))-((int)((((int)(b - d)) >>((int)(b)))))+((long)((((int)(d)) &((int)(b - d))))))))))-((long)((((int)(b - d + 42 +((long)((((double)(r)) -((double)(r)))))-((int)((((double)(b - d)) -((double)(d)))))-((long)((((int)(b - d)) ^((int)(d)))))+((int)((((double)(b - d)) *((double)(b)))))-((int)((((int)(d)) >>((int)(b - d)))))-((short)((((int)(b)) >>((int)(r)))))-((int)((((int)(b - d)) >>((int)(b)))))+((long)((((int)(d)) &((int)(b - d))))))) ^((int)(b - d + 42 +((long)((((double)(r)) -((double)(r)))))-((int)((((double)(b - d)) -((double)(d)))))-((long)((((int)(b - d)) ^((int)(d)))))+((int)((((double)(b - d)) *((double)(b)))))-((int)((((int)(d)) >>((int)(b - d)))))-((short)((((int)(b)) >>((int)(r)))))-((int)((((int)(b - d)) >>((int)(b)))))+((long)((((int)(d)) &((int)(b - d))))))))))+((int)((((int)(b - d + 42 +((long)((((double)(r)) -((double)(r)))))-((int)((((double)(b - d)) -((double)(d)))))-((long)((((int)(b - d)) ^((int)(d)))))+((int)((((double)(b - d)) *((double)(b)))))-((int)((((int)(d)) >>((int)(b - d)))))-((short)((((int)(b)) >>((int)(r)))))-((int)((((int)(b - d)) >>((int)(b)))))+((long)((((int)(d)) &((int)(b - d))))))) &((int)(r)))))-((int)((((int)(b - d + 42 +((long)((((double)(r)) -((double)(r)))))-((int)((((double)(b - d)) -((double)(d)))))-((long)((((int)(b - d)) ^((int)(d)))))+((int)((((double)(b - d)) *((double)(b)))))-((int)((((int)(d)) >>((int)(b - d)))))-((short)((((int)(b)) >>((int)(r)))))-((int)((((int)(b - d)) >>((int)(b)))))+((long)((((int)(d)) &((int)(b - d))))))) >>((int)(b - d + 42 +((long)((((double)(r)) -((double)(r)))))-((int)((((double)(b - d)) -((double)(d)))))-((long)((((int)(b - d)) ^((int)(d)))))+((int)((((double)(b - d)) *((double)(b)))))-((int)((((int)(d)) >>((int)(b - d)))))-((short)((((int)(b)) >>((int)(r)))))-((int)((((int)(b - d)) >>((int)(b)))))+((long)((((int)(d)) &((int)(b - d))))))))))-((short)((((int)(r)) >>((int)(r)))))-((int)((((int)(b - d + 42 +((long)((((double)(r)) -((double)(r)))))-((int)((((double)(b - d)) -((double)(d)))))-((long)((((int)(b - d)) ^((int)(d)))))+((int)((((double)(b - d)) *((double)(b)))))-((int)((((int)(d)) >>((int)(b - d)))))-((short)((((int)(b)) >>((int)(r)))))-((int)((((int)(b - d)) >>((int)(b)))))+((long)((((int)(d)) &((int)(b - d))))))) >>((int)(r)))))+((long)((((int)(b - d + 42 +((long)((((double)(r)) -((double)(r)))))-((int)((((double)(b - d)) -((double)(d)))))-((long)((((int)(b - d)) ^((int)(d)))))+((int)((((double)(b - d)) *((double)(b)))))-((int)((((int)(d)) >>((int)(b - d)))))-((short)((((int)(b)) >>((int)(r)))))-((int)((((int)(b - d)) >>((int)(b)))))+((long)((((int)(d)) &((int)(b - d))))))) &((int)(b - d + 42 +((long)((((double)(r)) -((double)(r)))))-((int)((((double)(b - d)) -((double)(d)))))-((long)((((int)(b - d)) ^((int)(d)))))+((int)((((double)(b - d)) *((double)(b)))))-((int)((((int)(d)) >>((int)(b - d)))))-((short)((((int)(b)) >>((int)(r)))))-((int)((((int)(b - d)) >>((int)(b)))))+((long)((((int)(d)) &((int)(b - d))))))))));
  return r;
}

int
main (void)
{
  int l = 8;
 asm ("" : "=r" (l) : "0" ((-(-2))));
 if (((int)((int)f (l + (-(-2)), l + (-(-3)), l + (-(-6))) != -(-(-3)) + 42 -((short)((((double)(-(-(-3)))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((int)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))+((long)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) *((double)(-(-(-3)))))))-((short)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) <<((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))*((short)((((int)(-(-(-3)))) &((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((short)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) |((int)(-(-(-3)))))))+((short)((((double)(-(-(-3)))) *((double)(-(-(-3)))))))*((int)((((int)(-(-(-3)))) <<((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((long)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) %((int)(-(-(-3)))))))+((long)((((int)(-(-(-3)))) |((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))) + 42 -((short)((((int)(-(-(-3)) + 42 -((short)((((double)(-(-(-3)))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((int)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))+((long)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) *((double)(-(-(-3)))))))-((short)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) <<((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))*((short)((((int)(-(-(-3)))) &((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((short)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) |((int)(-(-(-3)))))))+((short)((((double)(-(-(-3)))) *((double)(-(-(-3)))))))*((int)((((int)(-(-(-3)))) <<((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((long)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) %((int)(-(-(-3)))))))+((long)((((int)(-(-(-3)))) |((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6)))))))))) %((int)((int)f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((int)((((int)((int)f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) %((int)(-(-(-3)) + 42 -((short)((((double)(-(-(-3)))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((int)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))+((long)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) *((double)(-(-(-3)))))))-((short)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) <<((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))*((short)((((int)(-(-(-3)))) &((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((short)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) |((int)(-(-(-3)))))))+((short)((((double)(-(-(-3)))) *((double)(-(-(-3)))))))*((int)((((int)(-(-(-3)))) <<((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6)))))))))))))+((long)((((int)(-(-(-3)) + 42 -((short)((((double)(-(-(-3)))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((int)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))+((long)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) *((double)(-(-(-3))))))))) &((int)(((short)((((double)(-(-(-3)))) *((double)(-(-(-3)))))))*((int)((((int)(-(-(-3)))) <<((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6)))))))))))))-((short)((((int)((int)f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) <<((int)((int)f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))*((short)((((int)(((short)((((double)(-(-(-3)))) *((double)(-(-(-3)))))))*((int)((((int)(-(-(-3)))) <<((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6)))))))))) &((int)(-(-(-3)) + 42 -((short)((((double)(-(-(-3)))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((int)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))+((long)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) *((double)(-(-(-3)))))))-((short)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) <<((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))*((short)((((int)(-(-(-3)))) &((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((short)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) |((int)(-(-(-3)))))))+((short)((((double)(-(-(-3)))) *((double)(-(-(-3)))))))*((int)((((int)(-(-(-3)))) <<((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6)))))))))))))-((short)((((int)(-(-(-3)) + 42 -((short)((((double)(-(-(-3)))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((int)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))+((long)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) *((double)(-(-(-3)))))))-((short)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) <<((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))*((short)((((int)(-(-(-3)))) &((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((short)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) |((int)(-(-(-3))))))))) |((int)(((long)((((int)(-(-(-3)))) |((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6)))))))))))))+((short)((((int)(((long)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) *((double)(-(-(-3))))))))) &((int)(((long)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) *((double)(-(-(-3))))))))))))*((int)((((int)(((short)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) <<((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))*((short)((((int)(-(-(-3)))) &((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6)))))))))) <<((int)(-(-(-3)) + 42 -((short)((((double)(-(-(-3)))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((int)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))+((long)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) *((double)(-(-(-3))))))))))))-((long)((((int)(-(-(-3)) + 42 -((short)((((double)(-(-(-3)))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((int)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))+((long)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) *((double)(-(-(-3)))))))-((short)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) <<((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))*((short)((((int)(-(-(-3)))) &((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((short)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) |((int)(-(-(-3))))))))) %((int)(((long)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) %((int)(-(-(-3))))))))))))+((long)((((int)(-(-(-3)) + 42 -((short)((((double)(-(-(-3)))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((int)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))+((long)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) *((double)(-(-(-3)))))))-((short)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) <<((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))*((short)((((int)(-(-(-3)))) &((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((short)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) |((int)(-(-(-3)))))))+((short)((((double)(-(-(-3)))) *((double)(-(-(-3)))))))*((int)((((int)(-(-(-3)))) <<((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((long)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) %((int)(-(-(-3)))))))+((long)((((int)(-(-(-3)))) |((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6)))))))))) |((int)(-(-(-3)) + 42 -((short)((((double)(-(-(-3)))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((int)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))+((long)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) *((double)(-(-(-3)))))))-((short)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) <<((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))*((short)((((int)(-(-(-3)))) &((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((short)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) |((int)(-(-(-3)))))))+((short)((((double)(-(-(-3)))) *((double)(-(-(-3)))))))*((int)((((int)(-(-(-3)))) <<((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6)))))))))))))))
  return 0;
}

Expected behaviour

Not to crash.

Actual behaviour

The program crashed with this trace:

[kernel] Warning: -slevel is a deprecated alias for option -eva-slevel.
  Please use -eva-slevel instead.
[kernel] Warning: -plevel is a deprecated alias for option -eva-plevel.
  Please use -eva-plevel instead.
[kernel] Warning: -val-warn-undefined-pointer-comparison is a deprecated alias
  for option -eva-warn-undefined-pointer-comparison.
  Please use -eva-warn-undefined-pointer-comparison instead.
[kernel] Warning: -no-val-alloc-returns-null is a deprecated alias
  for option -eva-no-alloc-returns-null.
  Please use -eva-no-alloc-returns-null instead.
[kernel] Warning: -val is a deprecated alias for option -eva. Please use -eva instead.
[kernel] Warning: -no-val-show-progress is a deprecated alias for option -eva-no-show-progress.
  Please use -eva-no-show-progress instead.
[kernel] Parsing 4ee67af5850fa1e85ef52301e74c7093eba28573.c (with preprocessing)
[eva] Option -eva-precision 5 detected, automatic configuration of the analysis:
  option -eva-min-loop-unroll set to 0 (default value).
  option -eva-auto-loop-unroll set to 128.
  option -eva-widening-delay set to 3 (default value).
  option -eva-partition-history set to 0 (default value).
  option -eva-slevel already set to 100.
  option -eva-ilevel set to 48.
  option -eva-plevel already set to 255 (not modified).
  option -eva-subdivide-non-linear set to 100.
  option -eva-remove-redundant-alarms set to true (default value).
  option -eva-domains set to 'cvalue,equality,gauges,octagon,symbolic-locations'.
  option -eva-split-return set to 'auto'.
  option -eva-equality-through-calls set to 'formals' (default value).
  option -eva-octagon-through-calls set to false (default value).
[eva] Splitting return states on:
[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] 4ee67af5850fa1e85ef52301e74c7093eba28573.c:17: Warning: 
  signed overflow. assert l + (int)(-((int)(-6))) ≤ 2147483647;
[eva:alarm] 4ee67af5850fa1e85ef52301e74c7093eba28573.c:6: Warning: 
  division by zero. assert d ≢ 0;
[eva:alarm] 4ee67af5850fa1e85ef52301e74c7093eba28573.c:6: Warning: 
  invalid RHS operand for shift. assert 0 ≤ b < 32;
[eva:alarm] 4ee67af5850fa1e85ef52301e74c7093eba28573.c:6: Warning: 
  signed overflow. assert d + 42 ≤ 2147483647;
[eva:alarm] 4ee67af5850fa1e85ef52301e74c7093eba28573.c:6: Warning: 
  signed overflow.
  assert -2147483648 ≤ (int)(d + 42) - (int)((short)((int)(b % d)));
[eva:alarm] 4ee67af5850fa1e85ef52301e74c7093eba28573.c:6: Warning: 
  signed overflow.
  assert (int)(d + 42) - (int)((short)((int)(b % d))) ≤ 2147483647;
[eva:alarm] 4ee67af5850fa1e85ef52301e74c7093eba28573.c:6: Warning: 
  division by zero.
  assert
  (int)((int)((int)(d + 42) - (int)((short)((int)(b % d)))) -
        (int)((short)((int)(b >> b))))
  ≢ 0;
[eva:alarm] 4ee67af5850fa1e85ef52301e74c7093eba28573.c:6: Warning: 
  signed overflow.
  assert
  (int)((int)((int)(d + 42) - (int)((short)((int)(b % d)))) -
        (int)((short)((int)(b >> b))))
  + 42 ≤ 2147483647;
[eva:alarm] 4ee67af5850fa1e85ef52301e74c7093eba28573.c:6: Warning: 
  signed overflow.
  assert
  b +
  (int)((int)((int)((int)((int)((int)(d + 42) - (int)((short)((int)(b % d)))) -
                          (int)((short)((int)(b >> b))))
                    + 42)
              -
              (int)((short)((int)(b %
                                  (int)((int)((int)(d + 42) -
                                              (int)((short)((int)(b % d))))
                                        - (int)((short)((int)(b >> b))))))))
        - (int)((short)((int)(b >> b))))
  ≤ 2147483647;
[kernel] Current source was: 4ee67af5850fa1e85ef52301e74c7093eba28573.c:8
  The full backtrace is:
  Raised at file "src/kernel_services/abstract_interp/ival.ml", line 267, characters 14-32
  Called from file "src/kernel_services/abstract_interp/ival.ml", line 281, characters 16-30
  Called from file "src/plugins/value/domains/octagons.ml", line 352, characters 11-43
  Called from file "src/plugins/value/domains/octagons.ml", line 360, characters 8-74
  Called from file "src/plugins/value/domains/octagons.ml", line 395, characters 19-48
  Called from file "src/plugins/value/domains/octagons.ml", line 1054, characters 6-77
  Called from file "src/plugins/value/domains/domain_product.ml", line 94, characters 6-42
  Called from file "src/plugins/value/domains/domain_product.ml", line 95, characters 6-44
  Called from file "src/plugins/value/domains/domain_product.ml", line 95, characters 6-44
  Called from file "src/plugins/value/domains/domain_product.ml", line 95, characters 6-44
  Called from file "src/plugins/value/engine/evaluation.ml", line 837, characters 36-73
  Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
  Called from file "src/plugins/value/engine/evaluation.ml", line 899, characters 6-34
  Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
  Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
  Called from file "src/plugins/value/engine/evaluation.ml", line 907, characters 6-33
  Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
  Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
  Called from file "src/plugins/value/engine/evaluation.ml", line 899, characters 6-34
  Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
  Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
  Called from file "src/plugins/value/engine/evaluation.ml", line 899, characters 6-34
  Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
  Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
  Called from file "src/plugins/value/engine/evaluation.ml", line 899, characters 6-34
  Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
  Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
  Called from file "src/plugins/value/engine/evaluation.ml", line 899, characters 6-34
  Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
  Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
  Called from file "src/plugins/value/engine/evaluation.ml", line 899, characters 6-34
  Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
  Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
  Called from file "src/plugins/value/engine/evaluation.ml", line 899, characters 6-34
  Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
  Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
  Called from file "src/plugins/value/engine/evaluation.ml", line 899, characters 6-34
  Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
  Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
  Called from file "src/plugins/value/engine/evaluation.ml", line 899, characters 6-34
  Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
  Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
  Called from file "src/plugins/value/engine/evaluation.ml", line 899, characters 6-34
  Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
  Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
  Called from file "src/plugins/value/engine/evaluation.ml", line 899, characters 6-34
  Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
  Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
  Called from file "src/plugins/value/engine/evaluation.ml", line 899, characters 6-34
  Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
  Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
  Called from file "src/plugins/value/engine/evaluation.ml", line 899, characters 6-34
  Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
  Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
  Called from file "src/plugins/value/engine/evaluation.ml", line 899, characters 6-34
  Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
  Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
  Called from file "src/plugins/value/engine/evaluation.ml", line 899, characters 6-34
  Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
  Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
  Called from file "src/plugins/value/engine/evaluation.ml", line 899, characters 6-34
  Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
  Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
  Called from file "src/plugins/value/engine/evaluation.ml", line 899, characters 6-34
  Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
  Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
  Called from file "src/plugins/value/engine/evaluation.ml", line 899, characters 6-34
  Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
  Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
  Called from file "src/plugins/value/engine/evaluation.ml", line 907, characters 6-33
  Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
  Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
  Called from file "src/plugins/value/engine/evaluation.ml", line 1103, characters 6-36
  Called from file "src/plugins/value/engine/subdivided_evaluation.ml", line 664, characters 25-60
  Called from file "src/plugins/value/engine/subdivided_evaluation.ml", line 602, characters 21-38
  Called from file "list.ml", line 121, characters 24-34
  Called from file "src/plugins/value/engine/subdivided_evaluation.ml", line 618, characters 23-76
  Called from file "src/plugins/value/engine/subdivided_evaluation.ml", line 685, characters 17-73
  Called from file "src/plugins/value/engine/evaluation.ml" (inlined), line 1148, characters 4-67
  Called from file "src/plugins/value/engine/evaluation.ml", line 1509, characters 23-77
  Called from file "src/plugins/value/engine/transfer_stmt.ml", line 157, characters 14-59
  Called from file "src/plugins/value/engine/transfer_stmt.ml", line 177, characters 4-54
  Called from file "src/plugins/value/engine/transfer_stmt.ml", line 251, characters 10-55
  Called from file "src/plugins/value/engine/iterator.ml" (inlined), line 233, characters 28-33
  Called from file "src/plugins/value/engine/iterator.ml", line 261, characters 4-60
  Called from file "src/plugins/value/partitioning/partition.ml", line 494, 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 494, characters 18-35
  Called from file "list.ml", line 92, characters 20-23
  Called from file "src/plugins/value/engine/iterator.ml", line 496, characters 18-60
  Called from file "src/plugins/value/engine/iterator.ml", line 543, characters 13-31
  Called from file "list.ml", line 110, characters 12-15
  Called from file "src/plugins/value/engine/iterator.ml" (inlined), line 540, characters 4-31
  Called from file "src/plugins/value/engine/iterator.ml", line 602, characters 6-22
  Called from file "src/plugins/value/engine/iterator.ml", line 769, characters 20-39
  Called from file "src/plugins/value/engine/compute_functions.ml", line 201, characters 8-45
  Called from file "src/plugins/value/engine/compute_functions.ml", line 221, characters 26-36
  Called from file "src/plugins/value/engine/transfer_stmt.ml", line 318, characters 10-43
  Called from file "src/plugins/value/engine/transfer_stmt.ml", line 456, characters 22-60
  Called from file "src/plugins/value/engine/transfer_stmt.ml", line 758, 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 754, characters 10-447
  Called from file "list.ml", line 121, characters 24-34
  Called from file "src/plugins/value/engine/transfer_stmt.ml", line 769, 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 742, characters 6-1023
  Called from file "src/plugins/value/engine/iterator.ml", line 274, characters 6-47
  Called from file "src/plugins/value/partitioning/partition.ml", line 494, 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 494, characters 18-35
  Called from file "list.ml", line 92, characters 20-23
  Called from file "src/plugins/value/engine/iterator.ml", line 496, characters 18-60
  Called from file "src/plugins/value/engine/iterator.ml", line 543, characters 13-31
  Called from file "list.ml", line 110, characters 12-15
  Called from file "src/plugins/value/engine/iterator.ml" (inlined), line 540, characters 4-31
  Called from file "src/plugins/value/engine/iterator.ml", line 602, characters 6-22
  Called from file "src/plugins/value/engine/iterator.ml", line 769, characters 20-39
  Called from file "src/plugins/value/engine/compute_functions.ml", line 201, characters 8-45
  Called from file "src/plugins/value/engine/compute_functions.ml", line 333, 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 842, characters 2-9
  Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 872, characters 18-64
  Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 231, characters 4-8
 
  Unexpected error (Abstract_interp.Error_Bottom).
  Please report as 'crash' at https://git.frama-c.com/pub/frama-c/issues
  Your Frama-C version is 22.0 (Titanium).
  Note that a version and a backtrace alone often do not contain enough
  information to understand the bug. Guidelines for reporting bugs are at:
  https://git.frama-c.com/pub/frama-c/-/wikis/Guidelines-for-reporting-bugs

Contextual information

  • Frama-C installation mode: Opam
  • Frama-C version: Frama-C version (as reported by frama-c -version) 22.0 (Titanium)
  • Plug-in used: eva
  • OS name: Ubuntu
  • OS version: 18

Additional information (optional)

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking