Library POLAR_library_functions_pp

Require Import C_expr C_pp.
Require Import POLAR_library_functions.

Local Open Scope string_scope.

Axiom pp_cmd_ssl_fetch_input : forall (x e1 : var) (e2:exp) (s:string),
  pp_cmd (PolarSSL.ssl_fetch_input x e1 e2) s = x ++ " = ssl_fetch_input(" ++ e1 ++ (", " ++ pp_exp e2 (");" ++ s)).

Axiom pp_cmd_memcpy : forall (x : var) (e1 e2 e3:exp) (s:string),
  pp_cmd (PolarSSL.memcpy x e1 e2 e3) s = x ++ " = memcpy(" ++ (pp_exp e1 (", " ++ pp_exp e2 (", " ++ pp_exp e3 (");" ++ s)))).

Axiom pp_cmd_memset : forall (x : var) (e1 e2 e3:exp) (s:string),
  pp_cmd (PolarSSL.memset x e1 e2 e3) s = x ++ " = memset(" ++ (pp_exp e1 (", " ++ pp_exp e2 (", " ++ pp_exp e3 (");" ++ s)))).

Axiom pp_cmd_md5_update : forall (e1 e2 e3:exp) (s:string),
  pp_cmd (PolarSSL.md5_update e1 e2 e3) s = "md5_update(" ++ pp_exp e1 (", " ++ pp_exp e2 (", " ++ pp_exp e3 (");" ++ s))).

Axiom pp_cmd_sha1_update : forall (e1 e2 e3:exp) (s:string),
  pp_cmd (PolarSSL.sha1_update e1 e2 e3) s = "sha1_update(" ++ pp_exp e1 (", " ++ pp_exp e2 (", " ++ pp_exp e3 (");" ++ s))).