aboutsummaryrefslogtreecommitdiff
path: root/dev/include
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2017-11-28 12:51:24 +0100
committerPierre-Marie Pédrot2017-11-28 13:34:47 +0100
commit8f47273f118808373649a3a084e4a3c99167edd3 (patch)
tree3a316928b3605cc9f87d6b630a45ccbe9b492152 /dev/include
parentd8093626b49b539bec283285ea37ba50e79f69d4 (diff)
Use safe demarshalling in the checker.
Instead of relying on the OCaml demarshaller, which is not resilient against ill-formed data, we reuse the safe demarshaller from votour. This ensures that garbage files do not trigger memory violations.
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions