The Grothendieck trace formula can be viewed as a generalization of the Lefschetz trace formula in étale cohomology from constant sheaves to constructible $l$-adic sheaves, but restricting to the Frobenius. I have heard that there is an extension of the Grothendieck trace formula to arbitrary morphisms, but don't know what it is. After some research it appears that it may be in SGA 5 Exposé 3 (judging by titles). Unfortunately I am having a hard time finding it because I do not know French and it is quite long. So my question is, what is the statement and even better, is there a more recent account of this work?