FStarLang/karamel

Unsound decimal literal extraction

pnmadelaine opened this issue · 1 comments

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;

Thanks for the report, interesting corner case!