Module Operator.Alarm

In the concrete, an alarm would correspond to an exception/panic due to a partial operator.

In the abstract, it corresponds to a (possible) error reported to the user.

Some transfer functions are partial: e.g. division by zero, loading at invalid addresses, arithmetic operation that overflow when overflowing is not permitted. When this situation happens in the analyzer, we raise an alarm.

TODO: we should add more information to better report what is the alarm. For instance, for overflows, we should tell what kind of operation created an overflow (add, sub, mul, div by -1, etc.), what kind of overflow (signed,unsigned, or unsigned + signed), etc.

TODO: We should raise the corresponding alarm as an exception in the concrete implementation too, to better document what is happening.

TODO: We should factorize and document each alarm.

type integer_overflow_type =

1. | Signed
2. | Unsigned
3. | Unsigned_signed

Signed means that both operations were signed, the result was signed and did not fit in size bits.

Unsigned means that both operations were unsigned, the result was unsigned and did not fit in size bits.

Unsigned_signed means that the first operation was unsigned, the second signed, the result was unsigned and did not fit in size bits.

type integer_overflow_operation =

1. | Biadd
2. | Bisub
3. | Bimul
4. | Bisdiv
5. | Bishl

Operation that triggered the overflow warning.

type _ t =

1. | Integer_overflow : {
   1. overflow_type : integer_overflow_type;
   2. size : Units.In_bits.t;
   3. operation : integer_overflow_operation;
   } -> [ `Any ] t
   (*

   An integer operation on bitvector overflows its type.

   *)
2. | Integer_underflow : {
   1. overflow_type : integer_overflow_type;
   2. size : Units.In_bits.t;
   3. operation : integer_overflow_operation;
   } -> [ `Any ] t
   (*

   An integer operation on bitvector underflows its type.

   *)
3. | Free_on_null_address : [ `Any ] t
4. | Extract_offset : [ `Any ] t
5. | Heap_typing : [ `Any ] t
6. | Weak_type : [ `Any ] t
7. | Weak_array_type : [ `Any ] t
8. | Array_offset_access : [ `Any ] t
9. | Load_param_nonptr : [ `Any ] t
10. | Store_param_nonptr : [ `Any ] t
11. | Load_param_nonptr_old : [ `Any ] t
12. | Incompatible_function_pointer : [ `Any ] t
13. | Incompatible_return_type : [ `Any ] t
14. | Impure_store : [ `Any ] t
15. | Manual_stub : [ `Any ] t
16. | Ptr_arith : [ `Any ] t
17. | Invalid_load_access : [ `Any ] t
18. | Invalid_store_access : [ `Any ] t
19. | Possibly_false_assertion : [ `Any ] t
20. | Unresolved_dynamic_jump : [ `Any ] t
21. | Weak_type_use : [ `Typing ] t
22. | Typing_store : [ `Typing ] t

This is a list of all alarms that can be raised by Codex

val show : 'a t -> string