package codex

  1. Overview
  2. Docs
The Codex library for building static analysers based on abstract interpretation

Install 

dune-project
 Dependency

codex.top Edit opam file Versions (1)

Authors

  1. M
    Matthieu Lemerre
  2. J
    Julien Simonnet
  3. O
    Olivier Nicole
  4. P
    Paul Robert
  5. D
    Dorian Lesbre
  6. I
    Iker Canut
  7. C
    Corentin Gendreau
  8. G
    Guillaume Girol
  9. C
    Charles Babu
  10. J
    Jérôme Faucheux

Maintainers

  1. M
    Matthieu Lemerre <matthieu.lemerre@cea.fr>

Sources

1.0-rc4.tar.gz
md5=bc7266a140c6886add673ede90e335d3
sha512=8da42c0ff2c1098c5f9cb2b5b43b306faf7ac93b8f5ae00c176918cee761f249ff45b29309f31a05bbcf6312304f86a0d5a000eb3f1094d3d3c2b9b4c7f5c386

doc/codex.operator/Operator/Alarm/index.html

Module Operator.AlarmSource

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.

Sourcetype 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.

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

Operation that triggered the overflow warning.

Sourcetype _ 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

Sourceval show : 'a t -> string