search

DeepSpec / InteractionTrees

A Library for Representing Recursive and Impure Programs in Coq
MIT License
194 stars 49 forks source link

Add printf as a library function #268

Closed rogerburtonpatel closed 3 weeks ago

rogerburtonpatel commented 3 weeks ago

tl;dr Hack in LLVM printf to use this project's current working implementation of puts. We might be able to follow these steps:

  1. Compile user printf as standard C printf to LLVMIR with clang
  2. Generalize to a standard library call that "only calls puts"
  3. Use our version of puts and be able to run whatever vellvm transformations we want with printf inside.
rogerburtonpatel commented 3 weeks ago

Closing as duplicate of https://github.com/vellvm/vellvm/issues/298. Updates will be posted there.