123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322(**************************************************************************)(* *)(* This file is part of Frama-C. *)(* *)(* Copyright (C) 2007-2023 *)(* CEA (Commissariat à l'énergie atomique et aux énergies *)(* alternatives) *)(* *)(* you can redistribute it and/or modify it under the terms of the GNU *)(* Lesser General Public License as published by the Free Software *)(* Foundation, version 2.1. *)(* *)(* It is distributed in the hope that it will be useful, *)(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)(* GNU Lesser General Public License for more details. *)(* *)(* See the GNU Lesser General Public License version 2.1 *)(* for more details (enclosed in the file licenses/LGPLv2.1). *)(* *)(**************************************************************************)openFormat_typesopenFormat_pprintexceptionInvalid_formatletwarnf=Options.Self.warning~current:true~wkey:Options.wkey_formatf(* ************************************************************************ *)(* printf format verification *)(* ************************************************************************ *)(* true = valid and useful,
false = valid but useless and
Invalid_format = invalid *)letcheck_flagspecflag=letcs=spec.f_conversion_specifierinmatchflag,cswith|FSharp,#has_alternative_form->true|FZero,#integer_specifierwhenOption.is_somespec.f_precision->warn"Flag 0 is ignored when a precision is specified";false|FZero,#numeric_specifierwhenList.memFMinusspec.f_flags->warn"Flag 0 is ignored when flag - is also specified.";false|FZero,#numeric_specifier->true|FMinus,cswhencs<>`n->true|FSpace,#signed_specifierwhenList.memFPlusspec.f_flags->warn"Flag ' ' is ignored when flag + is also specified.";false|FSpace,#signed_specifier->true|FPlus,(#signed_specifier|#float_specifier)->true|_->warn"Flag %a and conversion specififer %a are not compatibles."pp_flagflagpp_cs(spec.f_conversion_specifier,spec.f_capitalize);raiseInvalid_formatletcheck_cs_compatibilitycscapitalizedhas_field_widthhas_precision=matchcswith|(`n|`c|`p)ascswhenhas_precision->warn"Conversion specifier %a does not expect a precision."pp_cs(cs,capitalized);raiseInvalid_format|`nwhenhas_field_width->warn"Conversion specifier n does not expect a field width.";raiseInvalid_format|_->()letrecmake_flags_unique=function|[]->[]|f::l->ifList.memflthen(warn"Multiple usage of flag '%a'."pp_flagf;make_flags_uniquel)elsef::make_flags_uniquel(* When checking, we don't really care which type are returned but only if
it can be returned *)letfind_typedef:Format_typer.typdef_finder=fun_namespace_name->Cil.voidTypeletcheck_f_specificationspec=(* Check the correctness of precision and field width fields *)check_cs_compatibilityspec.f_conversion_specifierspec.f_capitalize(spec.f_precision<>None)(spec.f_field_width<>None);(* Check the combination of conversion specifier and length modifier *)begintryignore(Format_typer.type_f_specifier~find_typedefspec)withFormat_typer.Invalid_specifier->warn"Length modifier %a and conversion specifier %a \
are not compatibles."(Pretty_utils.pp_optpp_lm)spec.f_length_modifierpp_cs(spec.f_conversion_specifier,spec.f_capitalize);raiseInvalid_formatend;(* Check and filter flags *)letflags=make_flags_uniquespec.f_flagsinletflags=List.filter(check_flagspec)flagsin{specwithf_flags=flags}letcheck_s_specificationspec=(* Check the correctness of field width *)check_cs_compatibilityspec.s_conversion_specifierfalsefalse(spec.s_field_width<>None);(* Check the combination of conversion specifier and length modifier *)begintryignore(Format_typer.type_s_specifier~find_typedefspec)withFormat_typer.Invalid_specifier->warn"Length modifier %a and conversion specifier %a \
are not compatibles."(Pretty_utils.pp_optpp_lm)spec.s_length_modifierpp_cs(spec.s_conversion_specifier,false);raiseInvalid_formatend;specletcheck_tokenf=function|Char_asc->c|Specifications->Specification(fs)letcheck_f_formatformat=List.map(check_tokencheck_f_specification)formatletcheck_s_formatformat=List.map(check_tokencheck_s_specification)formatletcheck_format=function|FFormatf->FFormat(check_f_formatf)|SFormats->SFormat(check_s_formats)(* ************************************************************************ *)(* Buffers *)(* ************************************************************************ *)moduleBuffer=structtypet=Format_string.t*intrefletcreate(s:Format_string.t):t=(s,ref0)letconsume(_s,i:t):unit=incriletback(_s,i:t):unit=decriletget(s,i:t):char=tryletc=Format_string.get_chars!iinincri;cwithFormat_string.OutOfBounds->'\000'|Format_string.NotAscii_->'\026'letlast(s,i:t):char=tryFormat_string.get_chars(!i-1)withFormat_string.OutOfBounds->'\000'|Format_string.NotAscii_->'\026'letpeek(s,i:t):char=tryFormat_string.get_chars!iwithFormat_string.OutOfBounds->'\000'|Format_string.NotAscii_->'\026'letgetall(f:char->bool)(s,iasb:t):string=letstart=!iinletlen=ref0inbegintrywhilef(getb)doincrlen;done;backb;(* last char has not been matched *)with_->()end;Format_string.sub_stringsstart!lenend(* ************************************************************************ *)(* Parsing *)(* ************************************************************************ *)letis_uppercase=function|'A'..'Z'->true|_->falseletrecparse_negativeb=matchBuffer.peekbwith|'-'->Buffer.consumeb;not(parse_negativeb)|_->falseletparse_intb=letneg=parse_negativebinlets=Buffer.getall(function'0'..'9'->true|_->false)binleti=tryint_of_stringswithFailure_->warn"Invalid integer in format.";raiseInvalid_formatinifnegthen-ielseiletparse_assignement_suppressionb=matchBuffer.peekbwith|'*'->Buffer.consumeb;true|_->falseletrecparse_flagsb=matchBuffer.getbwith|'-'->FMinus::parse_flagsb|'+'->FPlus::parse_flagsb|' '->FSpace::parse_flagsb|'#'->FSharp::parse_flagsb|'0'->FZero::parse_flagsb|_->Buffer.backb;[]letparse_f_fwb=matchBuffer.peekbwith|'*'->Buffer.consumeb;Some`FWStar|'0'..'9'->Some(`FWInt(parse_intb))|_->Noneletparse_s_fwb=matchBuffer.peekbwith|'0'..'9'->Some(`FWInt(parse_intb))|_->Noneletparse_precisionb=matchBuffer.peekbwith|'.'->Buffer.consumeb;SomebeginmatchBuffer.peekbwith|'*'->Buffer.consumeb;PStar|'-'|'0'..'9'->PInt(parse_intb)|_->PInt0end|_->Noneletparse_lmb=matchBuffer.getb,Buffer.peekbwith|'h','h'->Buffer.consumeb;Some`hh|'h',_->Some`h|'l','l'->Buffer.consumeb;Some`ll|'l',_->Some`l|'j',_->Some`j|'z',_->Some`z|'t',_->Some`t|'L',_->Some`L|_->Buffer.backb;Noneletparse_brackets_interiorb=letfirst=reftrueandcirc=reffalseinletmatching=function|']'whennot!first->false|'^'when!first&¬!circ->circ:=true;true|'\000'->warn"Unterminated brackets.";raiseInvalid_format|_->first:=false;trueinlets=Buffer.getallmatchingbinBuffer.consumeb;sletparse_f_csb=matchBuffer.getbwith|'d'->`d|'i'->`i|'o'->`o|'u'->`u|'c'->`c|'s'->`s|'p'->`p|'n'->`n|'x'|'X'->`x|'f'|'F'->`f|'e'|'E'->`e|'g'|'G'->`g|'a'|'A'->`a|'\000'->warn"Missing conversion specifier at the end of format.";raiseInvalid_format|'\026'->warn"Conversion specifiers must be ascii characters.";raiseInvalid_format|c->warn"Unknown conversion specifier %c."c;raiseInvalid_formatletparse_s_csb=matchBuffer.peekbwith|'['->Buffer.consumeb;`Brackets(parse_brackets_interiorb)|_->parse_f_csbletparse_f_specb=letf_flags=parse_flagsbinletf_field_width=parse_f_fwbinletf_precision=parse_precisionbinletf_length_modifier=parse_lmbinletf_conversion_specifier=parse_f_csbinletf_capitalize=is_uppercase(Buffer.lastb)incheck_f_specification{f_flags;f_field_width;f_precision;f_length_modifier;f_conversion_specifier;f_capitalize}letparse_s_specb=lets_assignment_suppression=parse_assignement_suppressionbinlets_field_width=parse_s_fwbinlets_length_modifier=parse_lmbinlets_conversion_specifier=parse_s_csbincheck_s_specification{s_assignment_suppression;s_field_width;s_length_modifier;s_conversion_specifier}letrecparse_auxfb=matchBuffer.getb,Buffer.peekbwith|'%','%'->Buffer.consumeb;(Char'%')::parse_auxfb|'%',_->letspec=fbinSpecificationspec::parse_auxfb|'\000',_->[]|c,_->Charc::parse_auxfbletparse_f_formats=parse_auxparse_f_spec(Buffer.creates)letparse_s_formats=parse_auxparse_s_spec(Buffer.creates)letparse_formattyps=matchtypwith|PrintfLike->FFormat(parse_f_formats)|ScanfLike->SFormat(parse_s_formats)