Unsound decimal literal extraction
pnmadelaine opened this issue · 1 comments
pnmadelaine commented
In FStar, a number literal with a leading zero is still interpreted as a decimal number.
In C, it is interpreted as octal.
When extracting, Karamel copies the full literal, with the leading zero(s).
For instance, the following FStar module:
module Bug
let literals_are_decimal () : Lemma (010 == 10) = ()
let octal : FStar.UInt32.t = FStar.UInt32.uint_to_t 010
let invalid_octal : FStar.UInt32.t = FStar.UInt32.uint_to_t 09
Extracts to the following C code:
#include "Bug.h"
uint32_t Bug_octal = (uint32_t)010U;
uint32_t Bug_invalid_octal = (uint32_t)09U;
msprotz commented
Thanks for the report, interesting corner case!