Copyright (C) 2019
This software is licensed under a dual BSD and GPL v2 license. See LICENSE file at the root folder of the project.
- Arnaud EBALARD (mailto:[email protected])
- Ryad BENADJILA (mailto:[email protected])
- Patricia MOUY (mailto:[email protected])
This software implements a X.509 certificate parser, annotated using ACSL annotations for verification with Frama-C.
The main Makefile is in the root directory, and compiling is as simple as executing:
$ make
This will compile different elements in the build directory:
- the x509-parser.o object file
- the x509-parser binary, which can be used on a DER certificate (or a concatenation of such elements)
The main Makefile has a Frama-C target which can be used to start Frama-C to verify the project.
$ make frama-c
Frama-C must have been installed prior to calling that target. Installing Frama-C can be done using OPAM. More details can be found on Frama-C project website. Frama-C may also be available as a common package on your distribution.