firefox-main/security/nss/lib/freebl/verified/karamel/include/krml
Name Description Size Coverage
c_endianness.h KRML_HEADER_ENDIAN_H 354 -
fstar_int.h Arithmetic Shift Right operator In all C standards, a >> b is implementation-defined when a has a signed type and a negative value. See e.g. 6.5.7 in http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2310.pdf GCC, MSVC, and Clang implement a >> b as an arithmetic shift. GCC: https://gcc.gnu.org/onlinedocs/gcc-9.1.0/gcc/Integers-implementation.html#Integers-implementation MSVC: https://docs.microsoft.com/en-us/cpp/cpp/left-shift-and-right-shift-operators-input-and-output?view=vs-2019#right-shifts Clang: tested that Clang 7, 8 and 9 compile this to an arithmetic shift We implement arithmetic shift right simply as >> in these compilers and bail out in others. 2499 -
internal -
lowstar_endianness.h / /* Implementing C.fst (part 2: endian-ness macros) 7422 -