aboutsummaryrefslogtreecommitdiffstats
path: root/riscV/Builtins1.v
Commit message (Expand)AuthorAgeFilesLines
* bits to floatDavid Monniaux2021-02-011-1/+9
* adding builtinsDavid Monniaux2021-02-011-4/+15
* Refine the type of function results in AST.signatureXavier Leroy2020-02-211-1/+1
* Give formal semantics to some built-in functions and run-time functionsXavier Leroy2019-07-171-0/+33